Verification, Model Checking, and Abstract Interpretation

DOI10.1007/b105073zbMath1111.68500OpenAlexW2611288859MaRDI QIDQ5711515

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

Publication date: 6 December 2005

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

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

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 (17)

Summarization for termination: No return! ⋮ Termination of Single-Path Polynomial Loop Programs ⋮ Recent advances in program verification through computer algebra ⋮ Termination of linear programs with nonlinear constraints ⋮ Generating exact nonlinear ranking functions by symbolic-numeric hybrid method ⋮ What else is undecidable about loops? ⋮ A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis ⋮ Unnamed Item ⋮ Proving termination of nonlinear command sequences ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ An Iterative Method for Generating Loop Invariants ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Proving Termination of Integer Term Rewriting ⋮ Automata-Based Termination Proofs ⋮ Ranking Functions for Linear-Constraint Loops ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ A second-order formulation of non-termination

This page was built for publication: Verification, Model Checking, and Abstract Interpretation