Computer Aided Verification

DOI10.1007/B11831zbMath1278.68164OpenAlexW1571340194MaRDI QIDQ5900703

Michael A. Colón, Sriram Sankaranarayanan, Henny B. Sipma

Publication date: 20 April 2010

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

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (37)

Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Lower-bound synthesis using loop specialization and Max-SMT ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Selectively-amortized resource bounding ⋮ Recent advances in program verification through computer algebra ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ Modular inference of subprogram contracts for safety checking ⋮ Constraint solving for interpolation ⋮ Deaccumulation techniques for improving provability ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ On invariant checking ⋮ Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ A unifying view on SMT-based software verification ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Subsequence Invariants ⋮ Improving Strategies via SMT Solving ⋮ Toward automatic verification of quantum programs ⋮ Property-directed incremental invariant generation ⋮ Automatic synthesis of \(k\)-inductive piecewise quadratic invariants for switched affine control programs ⋮ From invariant checking to invariant inference using randomized search ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Constructing invariants for hybrid systems ⋮ Elimination Techniques for Program Analysis ⋮ Loop invariants ⋮ Inferring Loop Invariants Using Postconditions ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration ⋮ Invariant Synthesis for Combined Theories ⋮ Static Analysis by Abstract Interpretation: A Mathematical Programming Approach ⋮ Speeding up the Constraint-Based Method in Difference Logic ⋮ Template polyhedra and bilinear optimization ⋮ Mathematics for reasoning about loop functions ⋮ O-Minimal Invariants for Discrete-Time Dynamical Systems

Uses Software

• QEPCAD
• REDLOG

This page was built for publication: Computer Aided Verification