Relative Completeness of Abstraction Refinement for Software Model Checking

No abstract is available for this paper.

• Publication year

  2002

• Venue

  International Conference on Tools and Algorithms for Construction and Analysis of Systems

• Publication date

  2002-04-08

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-46002-0_12
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Counterexample-guided abstraction refinement

  2003cited by this paper
• Automatic predicate abstraction of C programs

  2001cited by this paper
• Incremental Verification by Abstraction

  2001influential reference
• Successive approximation of abstract transition relations

  2001cited by this paper
• Automatically validating temporal safety properties of interfaces

  2001influential reference
• Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking

  2001cited by this paper
• A Classification of Symbolic Transition Systems

  2000cited by this paper
• Counterexample-Guided Abstraction Refinement

  2000cited by this paper
• Bandera: extracting finite-state models from Java source code

  2000cited by this paper
• Syntactic Program Transformations for Automatic Abstraction

  2000cited by this paper
• Dynamic Partitioning in Linear Relation Analysis. Application to the Verification of Synchronous Programs

  2000cited by this paper
• Counterexample-guided Abstraction Reenement

  2000cited by this paper
• Experience with Predicate Abstraction

  1999cited by this paper
• Parametric shape analysis via 3-valued logic

  1999cited by this paper
• On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction

  1999cited by this paper
• Model Checking in CLP

  1999cited by this paper
• Abstract and Model Check While You Prove

  1999cited by this paper
• Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis

  1999cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• HYTECH: the next generation

  1995cited by this paper
• Verification of Linear Hybrid Systems by Means of Convex Approximations

  1994cited by this paper
• Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation

  1992cited by this paper
• Graph-Based Algorithms for Boolean Function Manipulation

  1986cited by this paper
• Systematic design of program analysis frameworks

  1979cited by this paper
• Automatic discovery of linear restraints among variables of a program

  1978cited by this paper
• Soundness and Completeness of an Axiom System for Program Verification

  1978cited by this paper

• Verification modulo theories

  2022cites this paper
• Accelerating Legacy String Kernels via Bounded Automata Learning

  2020influential citation
• Improving Programming Support for Hardware Accelerators Through Automata Processing Abstractions

  2020influential citation
• Software Engineering Tools: Compatability and Integration

  2019influential citation
• Formal verification-driven parallelisation synthesis

  2018cites this paper
• Infinite-state invariant checking with IC3 and predicate abstraction

  2016cites this paper
• On recursion-free Horn clauses and Craig interpolation

  2014cites this paper
• Making abstract models complete †

  2014cites this paper
• Automated proof-producing abstraction of C code

  2014cites this paper
• Parallel Methods of Solving of Supply Problem Using Ant Colony Optimization

  2013cites this paper
• Data Abstraction in Coordination Constraints

  2013cites this paper
• Classifying and Solving Horn Clauses for Verification

  2013cites this paper
• The Relationship between Craig Interpolation and Recursion-Free Horn Clauses

  2013cites this paper
• Sigma*: symbolic learning of input-output specifications

  2013cites this paper
• Software Model Checking for People Who Love Automata

  2013cites this paper
• Three-valued abstraction and heuristic-guided refinement for verifying concurrent systems

  2013cites this paper
• Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)

  2013cites this paper
• Sigma*: Symbolic Learning of Stream Filters

  2012cites this paper
• Accelerating Interpolants

  2012cites this paper
• A hoare calculus for the verification of synchronous languages

  2012cites this paper
• RELATIONAL VERIFICATION OF PROGRAMS WITH INTEGER DATA

  2012cites this paper
• Vérification relationnelle pour des programmes avec des données entières

  2012cites this paper
• DOCTEUR DE L'UNIVERSITÉ DE GRENOBLE

  2012cites this paper
• Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux

  2012cites this paper
• Static Verification Tools for C Programs and Linux Device Drivers: A Survey

  2012cites this paper
• Heuristic-Guided Abstraction Refinement for Concurrent Systems

  2012cites this paper
• Verification of multi-linked heaps

  2012cites this paper
• Symbolic Grey-Box Learning of Input-Output Relations

  2012influential citation
• Software Model Checking by Program Specialization

  2012cites this paper
• Accelerating Interpolants ⋆

  2012cites this paper
• TRACER: A Symbolic Execution Tool for Verification

  2012cites this paper
• Una contribución a las técnicas avanzadas de verificación de procesos de negocio y sistemas software abiertos

  2011cites this paper
• An Introduction to Practical Formal Methods Using Temporal Logic

  2011cites this paper
• Verification and falsification of programs with loops using predicate abstraction

  2010cites this paper
• Program analysis with interpolants

  2010cites this paper
• Automated Invariant Generation for the Verification of Real-Time Systems

  2010cites this paper
• préparée au laboratoire Vérimag sous la direction de Nicolas Halbwachs dans le cadre de l'École Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique

  2010cites this paper
• Compiler-Assisted Software Model Checking and Monitoring

  2010cites this paper
• Logical Abstract Domains and Interpretations

  2010cites this paper
• Size-Change Termination and Transition Invariants

  2010cites this paper
• SLAM2: Static driver verification with under 4% false alarms

  2010cites this paper
• Non-monotonic Refinement of Control Abstraction for Concurrent Programs

  2010cites this paper
• Software model checking

  2009cites this paper
• Combining Theories with Shared Set Operations

  2009cites this paper
• Relaxation Refinement: A New Method to Generate Heuristic Functions

  2009cites this paper
• Automated Predicate Abstraction for Real-Time Models

  2009cites this paper
• Abstraction Refinement for Quantified Array Assertions

  2009influential citation
• Refinement of Trace Abstraction

  2009cites this paper
• Explorer Abstraction Refinement for Quantified Array Assertions

  2009influential citation
• Incomplete property checking for asynchronous reactive systems

  2008influential citation
• Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?

  2008cites this paper
• Program Model Checking: A Practitioner's Guide

  2008cites this paper
• Culling predicates for the Verification of Real-Time Models

  2008cites this paper
• Security Assessment Framework Using Static Analysis and Fault Injection

  2008cites this paper
• A prototype implementation of a distributed Satisfiability Modulo Theories solver in the ToolBus framework

  2008cites this paper
• Path invariants

  2007cites this paper
• Fixpoint-Guided Abstraction Refinements

  2007cites this paper
• The Future of Software Engineering

  2007cites this paper
• Distributing the Workload in a Lazy Theorem-Prover

  2007cites this paper
• ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement

  2007influential citation
• Modular Ranking Abstraction

  2007cites this paper
• Shape analysis by augmentation, abstraction, and transformation

  2007cites this paper
• Model checking with abstraction refinement for well-structured systems

  2006cites this paper
• A Practical and Complete Approach to Predicate Refinement

  2006cites this paper
• Comparing Completeness Properties of Static Analyses and Their Logics

  2006influential citation
• Thorough static analysis of device drivers

  2006cites this paper
• A logic and decision procedure for verification of heap-manipulating programs

  2006cites this paper
• Reduction and Abstraction Techniques for Model Checking

  2006cites this paper
• A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs

  2006cites this paper
• A Model for Security Vulnerability Pattern

  2006cites this paper
• Abstraction in Software Model Checking

  2006cites this paper
• Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems

  2006cites this paper
• Shape Analysis by Predicate Abstraction

  2005cites this paper
• Secure Information Flow as a Safety Problem

  2005cites this paper
• Abstract Model Checking of tccp programs

  2005cites this paper
• Ranking Abstraction as Companion to Predicate Abstraction

  2005cites this paper
• Counterexample Refinement for a Boundedness Test for CFSM Languages

  2005influential citation
• Verifying Time Partitioning in the DEOS Scheduling Kernel

  2005cites this paper
• Deductive mechanical verification of concurrent systems

  2005cites this paper
• Ranking Abstraction as a Companion to Predicate Abstraction,

  2005cites this paper
• On the Role of Static Analysis in Operating System Checking and Runtime Verification

  2005cites this paper
• Checking universally quantified temporal properties with three-valued analysis

  2005cites this paper
• Counterexample-Based Refinement for a Boundedness Test for CFSM Languages

  2005cites this paper
• Generalized Typestate Checking for Data Structure Consistency

  2005cites this paper
• Data-abstraction refinement: a game semantic approach

  2005influential citation
• FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs

  2005cites this paper
• A semantic framework for the abstract model checking of tccp programs

  2005cites this paper
• Boolean Algebra of Shape Analysis Constraints

  2004cites this paper
• Programmanalyse des XRTL-Zwischencodes

  2004cites this paper
• SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft

  2004cites this paper
• Temporal verification with transition invariants

  2004cites this paper
• On Our Experience with Modular Pluggable Analyses

  2004cites this paper
• Generalized Records and Spatial Conjunction in Role Logic

  2004cites this paper
• Symbolic Shape Analysis Diploma Thesis

  2004cites this paper
• Heuristic-guided counterexample search in FLAVERS

  2004cites this paper
• Localizing Program Errors for Cimple Debugging

  2004cites this paper
• Verification of Java Programs Using Symbolic Execution and Invariant Generation

  2004cites this paper
• Formal Techniques for Networked and Distributed Systems – FORTE 2004

  2004cites this paper
• Counterexample Guided Abstraction Refinement Via Program Execution

  2004cites this paper
• A static analyzer for large safety-critical software

  2003cites this paper