Verification, Model Checking, and Abstract Interpretation

DOI10.1007/b94790zbMath1202.68109MaRDI 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

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

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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