Counterexample guided path reduction for static program analysis

DOI10.1007/978-3-642-11512-7_20MaRDI QIDQ5187836zbMATH OpenOpenAlexFDO

Authors Ansgar Fehnker, Ralf Huuck, Sean Seefried

Publication date 9 March 2010

Published in Concurrency, Compositionality, and Correctness (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11512-7_20

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Incremental false path elimination for static software analysis
• SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
• Thread-modular counterexample-guided abstraction refinement
• Dynamic Path Reduction for Software Model Checking
• Application of static analyses for state-space reduction to the microcontroller binary code

Cites work

• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
• Precise Fixpoint Computation Through Strategy Iteration
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra

Cited in

(5)

• scientific article; zbMATH DE number 2090852 (Why is no real title available?)
• SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
• Application of static analyses for state-space reduction to the microcontroller binary code
• Program analysis via satisfiability modulo path programs
• Incremental false path elimination for static software analysis

Describes a project that uses

Uses Software

• SatAbs
• Orion
• Goanna
• BLAST

This page was built for publication: Counterexample guided path reduction for static program analysis

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