[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Dutertre et al., 2006 - Google Patents

The yices smt solver

Dutertre et al., 2006

View PDF
Document ID
8251242406333355860
Author
Dutertre B
De Moura L
Publication year
Publication venue
Tool paper at http://yices. csl. sri. com/tool-paper. pdf

External Links

Snippet

SMT stands for Satisfiability Modulo Theories. An SMT solver decides the satisfiability of propositionally complex formulas in theories such as arithmetic and uninterpreted functions with equality. SMT solving has numerous applications in automated theorem proving, in …
Continue reading at citeseerx.ist.psu.edu (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5009—Computer-aided design using simulation
    • G06F17/504—Formal methods
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/46—Multiprogramming arrangements
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G06F17/5045—Circuit design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/455—Emulation; Software simulation, i.e. virtualisation or emulation of application or operating system execution engines
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/10—Complex mathematical operations
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F2217/00—Indexing scheme relating to computer aided design [CAD]

Similar Documents

Publication Publication Date Title
Dutertre et al. The yices smt solver
Fränzle et al. HySAT: An efficient proof engine for bounded model checking of hybrid systems
Burch et al. Symbolic model checking for sequential circuit verification
Gregory et al. Planning modulo theories: Extending the planning paradigm
Seger et al. An industrially effective environment for formal hardware verification
Sampaio An algebraic approach to compiler design
KR100237090B1 (en) Centralized control system
Wang et al. An improved HHL prover: an interactive theorem prover for hybrid systems
Liebrenz et al. Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X
Swords et al. Bit-blasting ACL2 theorems
Li et al. SAT-based explicit LTL reasoning
Paulson Mechanizing UNITY in isabelle
Laurent et al. Assuring the guardians
Jifeng et al. A hybrid relational modelling language
McIver et al. Towards automated proof support for probabilistic distributed systems
Van Eijk et al. A verification framework for agent communication
Hüttel Transitions and trees: an introduction to structural operational semantics
Burch et al. Symbolic model checking for sequential circuit verification
Huerta y Munive Algebraic verification of hybrid systems in Isabelle/HOL
Jones et al. Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
Sogokon et al. Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
Butterfield et al. prialt in Handel-C: an operational semantics
Ma et al. The infinite evolution mechanism of ϵ-bisimilarity
Brucker et al. Formally verified interval arithmetic and its application to program verification
Borba et al. Refinement of concurrent object oriented programs