Automatic verification by abstract interpretation

DOI10.1007/3-540-36384-X_4MaRDI QIDQ4414376zbMATH OpenFDO

Authors Patrick Cousot

Publication date 25 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2575/25750020.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic verification based on abstract interpretation
• Abstract Interpretation as Automated Deduction
• Verification by abstract interpretation
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• scientific article; zbMATH DE number 1497823

Cited in

(38)

• Automating regression verification of pointer programs by predicate abstraction
• Verified functional programming of an abstract interpreter
• Abstract interpretation as automated deduction
• Abstract interpretation of microcontroller code: intervals meet congruences
• Abstraction-based partial deduction for solving inverse problems -- a transformational approach to software verification. (Extended abstract)
• Automatic verification based on abstract interpretation
• Incremental verification by abstraction
• Automating abstract interpretation
• An automata-based approach to trace partitioned abstract interpretation
• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Bridging the Gap: Automatic Verified Abstraction of C
• Program security verification based on abstract invariants
• How to transform an analyzer into a verifier
• Verification of concrete programs with respect to abstract programs
• Abstract Interpretation as Automated Deduction
• Gamifying program analysis
• Automated discovery of simulation between programs
• Abstract Interpretation with Applications to Timing Validation
• Static analysis, abstract interpretation and verification in (constraint logic) programming
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
• Automatic abstraction using generalized model checking
• Abstracting induction by extrapolation and interpolation
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules
• Automatic abstraction for bit-vectors using decision procedures
• Counterexample-guided focus
• Verification by abstract interpretation
• Automated verification of relational while-programs
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Computer Aided Verification
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Verification by augmented abstraction: The automata-theoretic view
• Automating the functional correspondence between higher-order evaluators and abstract machines
• String abstraction for model checking of C programs
• Trace Abstraction-Based Verification for Uninterpreted Programs
• Abstract interpretation of recursive logic definitions for efficient runtime assertion checking
• Automatic program instrumentation for automatic verification
• Verifying numerical programs via iterative abstract testing

This page was built for publication: Automatic verification by abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4414376)