Verification, Model Checking, and Abstract Interpretation

DOI10.1007/b94790zbMath1202.68109OpenAlexW3146639584MaRDI QIDQ5901912

Andrey Rybalchenko, Andreas Podelski

Publication date: 15 May 2009

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

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

Mathematics Subject Classification ID

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

Related Items

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ On the Termination of Integer Loops ⋮ Reflections on termination of linear loops ⋮ Decision tree learning in CEGIS-based termination analysis ⋮ Predicate Abstraction for Program Verification ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Termination of Single-Path Polynomial Loop Programs ⋮ A Hoare Logic for Energy Consumption Analysis ⋮ Convergence: integrating termination and abort-freedom ⋮ Recent advances in program verification through computer algebra ⋮ Complexity and resource bound analysis of imperative programs using difference constraints ⋮ Generating exact nonlinear ranking functions by symbolic-numeric hybrid method ⋮ On invariant checking ⋮ What's decidable about discrete linear dynamical systems? ⋮ Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis ⋮ A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis ⋮ Closed-form upper bounds in static cost analysis ⋮ Temporal property verification as a program analysis task ⋮ Efficiently solving quantified bit-vector formulas ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Proving termination of nonlinear command sequences ⋮ Efficient solution of a class of quantified constraints with quantifier prefix exists-forall ⋮ Transition Invariants and Transition Predicate Abstraction for Program Termination ⋮ Property-directed incremental invariant generation ⋮ Termination of polynomial loops ⋮ Proving Termination Through Conditional Termination ⋮ Ranking function synthesis for bit-vector relations ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ A new representation and associated algorithms for generalized planning ⋮ Automatic Verification of Counter Systems With Ranking Function ⋮ A new look at the automatic synthesis of linear ranking functions ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Extended Nested Dual System Groups, Revisited ⋮ Automated Program Verification ⋮ Decision Procedures for Automating Termination Proofs ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Unnamed Item ⋮ Lower Runtime Bounds for Integer Programs ⋮ Speeding up the Constraint-Based Method in Difference Logic ⋮ Proving Termination of Integer Term Rewriting ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Ranking Functions for Linear-Constraint Loops ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ Algebraic model checking for discrete linear dynamical systems ⋮ Type-based analysis of logarithmic amortised complexity ⋮ Witness to non-termination of linear programs ⋮ Runtime complexity analysis of logically constrained rewriting