Property-directed incremental invariant generation
type: Item
instance of: scholarly article
title: Property-directed incremental invariant generation
zbMATH Open document ID: 1149.68402
author: Aaron R. Bradley
author: Zohar Manna
published in: Formal Aspects of Computing
publication date: 2008-08-21T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 5314960
zbMATH Keywords: Static analysis
zbMATH Keywords: Model checking
zbMATH Keywords: Invariant generation
zbMATH Keywords: Affine invariants
zbMATH Keywords: Polynomial invariants
zbMATH Keywords: Clausal invariants
describes a project that uses: Mathematica
describes a project that uses: Chaff
MaRDI profile type: Publication
full work available at URL: s00165-008-0080-9
OpenAlex ID: W1973291036
cites work: SAT-based induction for temporal safety properties
cites work: Introduction to set constraint-based program analysis
cites work: Termination criteria for bounded model checking: extensions and comparison
cites work: Computational experience with the reverse search vertex enumeration algorithm
cites work: Symbolic model checking: \(10^{20}\) states and beyond
cites work: Verification Constraint Problems with Strengthening
cites work: Q5310200
cites work: Computer Aided Verification
cites work: Structured and simultaneous Lyapunov functions for system stability problems
cites work: Q2754081
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Q2769578
cites work: Q4804915
cites work: Q5584402
cites work: Affine relationships among variables of a program
cites work: Q4417909
cites work: Q4804900
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Q4873991
cites work: Hybrid Systems: Computation and Control
cites work: Analysis of Non-polynomial Systems Using the Sum of Squares Decomposition
cites work: Q3818127
cites work: Verification: Theory and Practice
cites work: Static Analysis
cites work: Q5807665
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Atsuji completions vis-à-vis hyperspaces
DOI: 10.1007/S00165-008-0080-9
description: scientific article; zbMATH DE number 5314960