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

Hoder et al., 2011 - Google Patents

Case studies on invariant generation using a saturation theorem prover

Hoder et al., 2011

View PDF
Document ID
4888842245628001971
Author
Hoder K
Kovács L
Voronkov A
Publication year
Publication venue
Mexican International Conference on Artificial Intelligence

External Links

Snippet

Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to …
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
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • 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
    • G06F17/11—Complex mathematical operations for solving equations, e.g. nonlinear equations, general mathematical optimization problems
    • 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/3061—Information retrieval; Database structures therefor; File system structures therefor of unstructured textual data
    • 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
    • G06F11/3668—Software testing
    • 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/20—Handling natural language data
    • G06F17/27—Automatic analysis, e.g. parsing
    • G06F17/2705—Parsing
    • 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
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
    • G06F21/55—Detecting local intrusion or implementing counter-measures
    • 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
    • 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
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N99/00—Subject matter not provided for in other groups of this subclass
    • G06N99/005—Learning machines, i.e. computer in which a programme is changed according to experience gained by the machine itself during a complete run
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N7/00—Computer systems based on specific mathematical models
    • G06N7/005—Probabilistic networks

Similar Documents

Publication Publication Date Title
Kovács et al. First-order theorem proving and Vampire
Solar-Lezama Program synthesis by sketching
Sharma et al. Knowledge Compilation meets Uniform Sampling.
Decker et al. Monitoring modulo theories
Jacobs et al. Featherweight verifast
Hahn et al. Constraint-based monitoring of hyperproperties
Marques-Silva et al. On using unsatisfiability for solving maximum satisfiability
Enea et al. On automated lemma generation for separation logic with inductive definitions
Gupta et al. : Weighted and Projected Sampling
Schneider et al. Automated reasoning for attributed graph properties
Daca et al. Abstraction-driven concolic testing
Fedyukovich et al. Automated discovery of simulation between programs
Hoder et al. Case studies on invariant generation using a saturation theorem prover
Kaliszyk et al. Certified connection tableaux proofs for HOL Light and TPTP
Reynolds et al. Reasoning in the bernays-schönfinkel-ramsey fragment of separation logic
Charwat et al. Dynamic Programming-based QBF Solving.
David et al. Using program synthesis for program analysis
Chapman et al. Learning the language of error
Schulte et al. When do bounds and domain propagation lead to the same search space?
Cook et al. Temporal property verification as a program analysis task: Extended Version
Bjørner et al. A practical integration of first-order reasoning and decision procedures
Beauquier et al. Security policies enforcement using finite and pushdown edit automata
Shkaravska et al. Test-based inference of polynomial loop-bound functions
Doutre et al. Abstract argumentation in dynamic logic: Representation, reasoning and change
Vakili et al. Finite model finding using the logic of equality with uninterpreted functions