Tools and Algorithms for the Construction and Analysis of Systems
From MaRDI portal
Publication:5899073
DOI10.1007/11691372zbMath1180.68118OpenAlexW2739785336MaRDI QIDQ5899073
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (28)
Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Constraint-based relational verification ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Verification of SpecC using predicate abstraction ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Interpolation and Model Checking ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Combining Predicate Abstraction with Fixpoint Approximations ⋮ Constraint solving for interpolation ⋮ SMT proof checking using a logical framework ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ From invariant checking to invariant inference using randomized search ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Counterexample Guided Path Reduction for Static Program Analysis ⋮ Interpolant Generation for UTVPI ⋮ Interpolation and Symbol Elimination ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Accelerating Interpolation-Based Model-Checking ⋮ Automatically Refining Abstract Interpretations ⋮ Partial predicate abstraction and counter-example guided refinement ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Under-approximating loops in C programs for fast counterexample detection ⋮ Refinement of Trace Abstraction ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
Uses Software
This page was built for publication: Tools and Algorithms for the Construction and Analysis of Systems
