Tools and Algorithms for the Construction and Analysis of Systems

DOI10.1007/11691372zbMATH Open1180.68118OpenAlexW2739785336MaRDI QIDQ5899073FDOQ5899073

Publication date: 2 May 2007

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

Full work available at URL: https://doi.org/10.1007/11691372

Recommendations

Predicate abstraction for program verification
Relaxed stratification: a new approach to practical complete predicate refinement
Tools and Algorithms for the Construction and Analysis of Systems
Predicate abstraction for software verification
Predicate Abstraction in Program Verification: Survey and Current Trends

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

Cited In (32)

Counterexample guided path reduction for static program analysis
Constraint-based relational verification
Latticed \(k\)-induction with an application to probabilistic programs
Combining Predicate Abstraction with Fixpoint Approximations
Abstract Counterexamples for Non-disjunctive Abstractions
Interpolant Generation for UTVPI
Interpolation and Symbol Elimination
From invariant checking to invariant inference using randomized search
Labelled interpolation systems for hyper-resolution, clausal, and local proofs
Interpolation and model checking
Relaxed stratification: a new approach to practical complete predicate refinement
Quantifier-free interpolation in combinations of equality interpolating theories
Efficient Interpolant Generation in Satisfiability Modulo Theories
An extension of lazy abstraction with interpolation for programs with arrays
Guiding Craig interpolation with domain-specific abstractions
Sharper and Simpler Nonlinear Interpolants for Program Verification
Accelerating Interpolation-Based Model-Checking
What Tipper is Ready for: A Semantics for Incomplete Predicates
Constraint solving for interpolation
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
Under-approximating loops in C programs for fast counterexample detection
Verification and falsification of programs with loops using predicate abstraction
Tools and Algorithms for the Construction and Analysis of Systems
Refinement of Trace Abstraction
Interpolation and symbol elimination in Vampire
Beyond quantifier-free interpolation in extensions of Presburger arithmetic
Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
Partial predicate abstraction and counter-example guided refinement
SMT proof checking using a logical framework
Verification of SpecC using predicate abstraction
Automatically Refining Abstract Interpretations

Uses Software

Chaff

This page was built for publication: Tools and Algorithms for the Construction and Analysis of Systems

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