Finite differencing of logical formulas for static analysis

DOI10.1007/3-540-36575-3_26MaRDI QIDQ4417906zbMATH OpenFDO

Authors Mooly Sagiv, Alexey Loginov, Thomas Reps

Publication date 30 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/2618/26180380.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Static analysis for logic-based dynamic programs
• Computer Aided Verification
• Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Computer Aided Verification

Cited in

(7)

• On the key dependent message security of the Fujisaki-Okamoto constructions
• View-augmented abstractions
• Logical Difference Computation with CEX2.5
• Sound and complete abstract graph transformation
• Bounded quantifier instantiation for checking inductive invariants
• A new representation and associated algorithms for generalized planning
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

Describes a project that uses

Uses Software

• TVLA

This page was built for publication: Finite differencing of logical formulas for static analysis

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