Computer Aided Verification

DOI10.1007/b138445zbMath1081.68611OpenAlexW2507913385MaRDI QIDQ5716591

Aaron R. Bradley, Henny B. Sipma, Zohar Manna

Publication date: 10 January 2006

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

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Related Items (19)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Reflections on termination of linear loops ⋮ Termination of Single-Path Polynomial Loop Programs ⋮ Convergence: integrating termination and abort-freedom ⋮ Constraint solving for interpolation ⋮ A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis ⋮ Unnamed Item ⋮ Property-directed incremental invariant generation ⋮ Proving Termination Through Conditional Termination ⋮ A new look at the automatic synthesis of linear ranking functions ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Proving mutual termination ⋮ Lower Runtime Bounds for Integer Programs ⋮ Proving Termination of Integer Term Rewriting ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Ranking Functions for Linear-Constraint Loops ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ Witness to non-termination of linear programs

This page was built for publication: Computer Aided Verification