Completeness and Complexity of Bounded Model Checking

No abstract is available for this paper.

• Publication year

  2004

• Venue

  International Conference on Verification, Model Checking and Abstract Interpretation

• Publication date

  2004-01-11

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-540-24622-0_9
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Bounded model checking

  2003cited by this paper
• SAT-based sequential depth computation

  2003cited by this paper
• Improving the Encoding of LTL Model Checking into SAT

  2002cited by this paper
• Property Checking via Structural Analysis

  2002cited by this paper
• Efficient Computation of Recurrence Diameters

  2002cited by this paper
• A Fixpoint Based Encoding for Bounded Model Checking

  2002cited by this paper
• Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

  2002influential reference
• Efficient Büchi Automata from LTL Formulae

  2000cited by this paper
• Symbolic Model Checking without BDDs

  1999influential reference
• On nested depth first search

  1996cited by this paper
• Simple on-the-fly automatic verification of linear temporal logic

  1995cited by this paper
• Another Look at LTL Model Checking

  1994cited by this paper
• The Temporal Logic of Reactive and Concurrent Systems

  1991cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• On the temporal analysis of fairness

  1980cited by this paper

• Automated Verification of Monotonic Data Structure Traversals in C

  2025cites this paper
• Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

  2024cites this paper
• Determining the Minimum Number of Virtual Networks for Different Coherence Protocols

  2024cites this paper
• Formal Analysis and Verification of Max-Plus Linear Systems

  2023cites this paper
• Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)

  2023cites this paper
• AutoHyper: Explicit-State Model Checking for HyperLTL

  2023cites this paper
• Completeness Thresholds for Memory Safety: Early Preliminary Report

  2022cites this paper
• Formal Verification of Safety Properties Using Interpolation and k-induction

  2022cites this paper
• Completeness Thresholds for Memory Safety of Array Traversing Programs

  2022cites this paper
• BMC-Based Temperature-Aware SBST for Worst-Case Delay Fault Testing Under High Temperature

  2022cites this paper
• SMT-Based Model Checking of Max-Plus Linear Systems

  2021cites this paper
• TOrPEDO: witnessing model correctness with topological proofs

  2021cites this paper
• Stateless software model checking parameterized with memory consistency models

  2020cites this paper
• Research on Formal Verification Method of Embedded Software Requirements Analysis Document

  2020cites this paper
• Computation of the Transient in Max-Plus Linear Systems via SMT-Solving

  2020cites this paper
• Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems

  2020cites this paper
• Survey on automated symbolic verification and its application for synthesising cyber-physical systems

  2020cites this paper
• Witness generation in existential CTL model checking

  2019cites this paper
• Probe Machine Based Computing Model for Solving Satisfiability Problem

  2019cites this paper
• Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

  2019cites this paper
• Electronic Communications of the EASST Volume 076 ( 2019 ) Automated Verification of Critical Systems 2018 ( AVoCS 2018 ) Writing a Model Checker in 80 Days : Reusable Libraries and Custom Implementation

  2019cites this paper
• Imprecision in WCET estimates due to library calls and how to reduce it (WIP paper)

  2019influential citation
• Verifying safety of synchronous fault-tolerant algorithms by bounded model checking

  2019cites this paper
• INtegrated TOol chain for model-based design of CPSs

  2019cites this paper
• Formally verified compositional algorithms for factored transition systems

  2018cites this paper
• Büchi Automata ( RQ 2 )

  2018cites this paper
• Efficient software product-line model checking using induction and a SAT solver

  2018cites this paper
• Towards Abstraction in ASP with an Application on Reasoning about Agent Policies

  2018cites this paper
• A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds

  2017cites this paper
• Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations

  2017cites this paper
• Linear templates of ACTL formulas with an application to SAT-based verification

  2017cites this paper
• Towards Infinite-State Symbolic Model Checking for B and Event-B

  2017cites this paper
• Para\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^2$$\end{document}2: parameterized path reduction, acceleration, a

  2017cites this paper
• Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing

  2016cites this paper
• Grant Agreement: 644047 INtegrated TOol chain for model-based design of CPSs

  2016cites this paper
• Critical Systems: Formal Methods and Automated Verification

  2016influential citation
• Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking

  2016cites this paper
• Grant Agreement : 644047 INtegrated TOol chain for model-based design of CPSs Implementation of a Model-Checking Component Deliverable

  2016cites this paper
• Model Checking and Model-Based Testing: Improving Their Feasibility by Lazy Techniques, Parallelization, and Other Optimizations

  2016cites this paper
• Parameterized Complexity Results for Symbolic Model Checking of Temporal Logics

  2016influential citation
• Achieving completeness in the verification of action theories by Bounded Model Checking in ASP

  2015influential citation
• Bounded semantics

  2015cites this paper
• Boolean Satisfiability Solvers and Their Applications in Model Checking

  2015cites this paper
• Parameterized Complexity Results for Agenda Safety in Judgment Aggregation

  2015cites this paper
• SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms

  2015cites this paper
• Bounded model checking of multi-threaded programs via sequentialization

  2015cites this paper
• Bounded model checking for asynchronous concurrent systems

  2014cites this paper
• Alternating Automata Semantic Constructions for the Bounded Model Checking of Regular Linear Temporal Logic ( Extended Version )

  2014cites this paper
• On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability

  2014cites this paper
• Combining Syntactic and Semantic Encoding for LTL Bounded Model Checking

  2014influential citation
• Automated Error-Detection and Repair for Compositional Software Specifications

  2014cites this paper
• Reconfigurable scan networks: formal verification, access optimization, and protection

  2014cites this paper
• Bounded Model Checking High Level Petri Nets in PIPE+Verifier

  2014cites this paper
• A tool for deciding the satisfiability of continuous-time metric temporal logic

  2013cites this paper
• The Parameterized Complexity of Reasoning Problems Beyond NP

  2013cites this paper
• SMT-Based Analysis of Biological Computation

  2013cites this paper
• Incremental, Inductive Model Checking

  2013cites this paper
• Counterexample-Preserving Reduction for Symbolic Model Checking

  2013cites this paper
• Incremental Semantic LTL Bounded Model Checking

  2013cites this paper
• Business process verification with constraint temporal answer set programming*

  2013cites this paper
• Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker

  2013cites this paper
• Quality and quantity in robustness checking using formal techniques

  2013cites this paper
• Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives

  2013influential citation
• Formal Verification and Synthesis for Quality-of-Service in On-Chip Networks

  2013cites this paper
• Efficient Bounded Model Checking for LTL

  2013cites this paper
• SAT-solving in CSP trace refinement

  2012cites this paper
• Automated Route Planning for Milk-run Transport Logistics Using Model Checking

  2012cites this paper
• Verification of Action Theories in ASP: A Complete Bounded Model Checking Approach

  2012influential citation
• Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata

  2012cites this paper
• Achieving Completeness in Bounded Model Checking of Action Theories in ASP

  2012influential citation
• The hidden models of model checking

  2012cites this paper
• A New Translation from ECTL* to SAT

  2012cites this paper
• SMT-Based Bounded Model Checking for Embedded ANSI-C Software

  2012cites this paper
• Techniques and tools for the verification of concurrent systems

  2012cites this paper
• Constraint LTL satisfiability checking without automata

  2012cites this paper
• Formal Techniques for Distributed Systems

  2012influential citation
• Z3-4Biology SMT-Based Analysis of Biological Computation

  2012cites this paper
• Approximating and Interpolating Theories of Arithmetic for Software Verification

  2011cites this paper
• Two Algorithms for Model Checking of Regular Linear Temporal Logic

  2011cites this paper
• Completeness of the Bounded Satisfiability Problem for Constraint LTL

  2011cites this paper
• Topological Structure of a Boolean Network

  2011cites this paper
• A SAT-Based Algorithm for Finding Attractors in Synchronous Boolean Networks

  2011cites this paper
• Linear Completeness Thresholds for Bounded Model Checking

  2011cites this paper
• Bounded Model Checking for Web Service Discovery and Composition

  2010cites this paper
• Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting

  2010influential citation
• A Linear Representation of Dynamics of Boolean Networks

  2010cites this paper
• Formal analysis of STM design with SAL infinite bounded model checker

  2010cites this paper
• SMT-based bounded model checking for multi-threaded software in embedded systems

  2010cites this paper
• SMT-Based Bounded Model Checking for Embedded ANSI-C Software

  2009cites this paper
• Bounded Semantics of CTL and SAT-Based Verification

  2009cites this paper
• Bounded Model Checking

  2009cites this paper
• Automatic Discovery of API-Level Vulnerabilities

  2008cites this paper
• Multi-level Bounded Model Checking to detect bugs beyond the bound

  2008cites this paper
• Nutzerfreundliche Modellierung mit hybriden Systemen zur symbolischen Simulation in CLP

  2008cites this paper
• Improving the Translation from ECTL to SAT

  2008cites this paper
• Improving Encoding Efficiency for Bounded Model Checking

  2008cites this paper
• Propositional Satisfiability: Algorithms and Applications

  2008cites this paper
• Modeling and verifying embedded operating systems

  2008cites this paper
• Verifying safety properties of Lustre programs: An SMT-based approach

  2008influential citation
• An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-Checking

  2008influential citation