Avoiding exponential explosion: generating compact verification conditions

No abstract is available for this paper.

• Publication year

  2001

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  Unknown publication date

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/360204.360220
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Boolean Programs: A Model and Process for Software Analysis

  2000cited by this paper
• Translation validation for an optimizing compiler

  2000cited by this paper
• Checking Java Programs via Guarded Commands

  1999influential reference
• Refinement Calculus: A Systematic Introduction

  1998cited by this paper
• The design and implementation of a certifying compiler

  1998influential reference
• Extended static checking

  1998cited by this paper
• An efficient method of computing static single assignment form

  1989cited by this paper
• A generalization of Dijkstra's calculus

  1989cited by this paper
• Detecting equality of variables in programs

  1988cited by this paper
• Techniques for program verification

  1979cited by this paper
• A Discipline of Programming

  1976cited by this paper

• Craig Interpolation in Program Verification

  2026cites this paper
• coma, an Intermediate Verification Language with Explicit Abstraction Barriers

  2025cites this paper
• Sound and Complete Invariant-Based Heap Encodings (Technical Report)

  2025cites this paper
• Verified VCG and Verified Compiler for Dafny

  2025cites this paper
• Automated Abstract Transformer Synthesis for Reduced Product Domains

  2025cites this paper
• Static Coverage in Deductive Software Verification

  2025cites this paper
• Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications

  2025cites this paper
• Computing Precise Control Interface Specifications

  2024influential citation
• A Program Instrumentation Framework for Automatic Verification

  2024cites this paper
• Synthesizing Abstract Transformers for Reduced-Product Domains

  2024cites this paper
• Learning to Locate and Describe Vulnerabilities

  2023cites this paper
• Correctness Witness Validation by Abstract Interpretation

  2023cites this paper
• Sound Runtime Assertion Checking for Memory Properties via Program Transformation

  2023influential citation
• Constructing Structured SSA from FJ

  2023cites this paper
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)

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

  2023cites this paper
• P4Cub: A Little Language for Big Routers

  2023cites this paper
• Verified symbolic execution with Kripke specification monads (and no meta-programming)

  2022cites this paper
• Symbolic encoding of LL(1) parsing and its applications

  2022cites this paper
• Certified Verification of Relational Properties

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

  2022cites this paper
• Tricera: Verifying C Programs Using the Theory of Heaps

  2022cites this paper
• Giant-step Semantics for the Categorisation of Counterexamples

  2021cites this paper
• A deductive reasoning approach for database applications using verification conditions

  2021cites this paper
• Toward optimal mc/dc test case generation

  2021cites this paper
• Formally Validating a Practical Verification Condition Generator (extended version)

  2021cites this paper
• Aquila: a practically usable verification system for production-scale programmable data planes

  2021cites this paper
• VeriOSS: Using the Blockchain to Foster Bug Bounty Programs

  2020cites this paper
• Treating for-Loops as First-Class Citizens in Proofs

  2020cites this paper
• bf4: towards bug-free P4 programs

  2020cites this paper
• Relational properties for specification and verification of C programs in Frama-C

  2019cites this paper
• A Generalized Program Verification Workflow Based on Loop Elimination and SA Form

  2019influential citation
• Proving Properties of Discrete-Valued Functions Using Deductive Proof: Application to the Square Root

  2019cites this paper
• Abstract Execution

  2019cites this paper
• Software Engineering Tools: Compatability and Integration

  2019cites this paper
• PROVING PROPERTIES OF DISCRETE-VALUED FUNCTIONS USING DEDUCTIVE PROOF: APPLICATION TO THE SQUARE ROOT

  2019cites this paper
• Checking Observational Purity of Procedures

  2019cites this paper
• IDVE: an integrated development and verification environment for JavaScript

  2019cites this paper
• Automatic Grading of Programming Assignments: An Approach Based on Formal Semantics

  2019influential citation
• Model-Agnostic Counterfactual Explanations for Consequential Decisions

  2019cites this paper
• Inferring Concise Specifications of APIs

  2019cites this paper
• Instrumenting a weakest precondition calculus for counterexample generation

  2018cites this paper
• Parse Condition: Symbolic Encoding of LL(1) Parsing

  2018cites this paper
• UCLID5: Integrating Modeling, Verification, Synthesis and Learning

  2018cites this paper
• Exploiting Pointer Analysis in Memory Models for Deductive Verification

  2018cites this paper
• Verifying Data-Oriented Gadgets in Binary Programs to Build Data-Only Exploits

  2018influential citation
• Provably Sound and Secure Automatic Proving and Generation of Verification Conditions

  2018influential citation
• Towards Robust and Flexible Intermediate Verification

  2018cites this paper
• Cycle-bounded model checking of PLC software via dynamic large-block encoding

  2018cites this paper
• p4v: practical verification for programmable data planes

  2018cites this paper
• An Introduction to Software Verification with Whiley

  2018cites this paper
• Improving Generalization in Software IC3

  2018cites this paper
• A Generalized Approach to Verification Condition Generation

  2018influential citation
• Triggerless Happy - Intermediate Verification with a First-Order Prover

  2017cites this paper
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows

  2017cites this paper
• Local refinement typing

  2017influential citation
• Bonsai: synthesis-based reasoning for type systems

  2017cites this paper
• Semantics-based generation of verification conditions via program specialization

  2017cites this paper
• Verification by Reduction to Functional Programs

  2017cites this paper
• RELSPEC: a framework for reliability aware design of component based embedded systems

  2017cites this paper
• A Value-based Memory Model for Deductive Verification

  2017cites this paper
• Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions

  2017cites this paper
• Technologies for finding errors in object-oriented software

  2017cites this paper
• Algorithms and Tools for Verification and Testing of Asynchronous Programs

  2016cites this paper
• Specification and Verification of Object-Oriented Software

  2016cites this paper
• Automated Verification of Functional Correctness of Race-Free GPU Programs

  2016cites this paper
• LLSPLAT: Improving Concolic Testing by Bounded Model Checking

  2016cites this paper
• Enhancing symbolic execution with veritesting

  2016cites this paper
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

  2016influential citation
• On-the-fly construction of provably correct service compositions - templates and proofs

  2016cites this paper
• Efficient reuse of learnt information for control-flow oriented IC3 algorithms

  2016cites this paper
• Software Reliability Analysis Using Weakest Preconditions in Linear Assignment Programs

  2016cites this paper
• Consiglio Nazionale delle Ricerche

  2016cites this paper
• Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution)

  2016cites this paper
• Precondition Calculation for Loops Iterating over Data Structures

  2016cites this paper
• Semantics-based generation of verification conditions by program specialization

  2015cites this paper
• Concurrent Bounded Model Checking

  2015cites this paper
• Interaction analysis of annotated specification and program codes in Extended Static Checking

  2015cites this paper
• Regression Verification for Programmable Logic Controller Software

  2015cites this paper
• A framework for the automatic verification of discrete-time MATLAB simulink models using Boogie

  2015cites this paper
• Evaluating control-flow based inductive model checking algorithms

  2015cites this paper
• Model Counting Modulo Theories

  2015cites this paper
• Flexible Goal-Directed Abstraction

  2015cites this paper
• Designing a verifying compiler: Lessons learned from developing Whiley

  2015cites this paper
• Computer-Aided Verification for Mechanism Design

  2015cites this paper
• Assertion-Directed Precondition Synthesis for Loops over Data Structures

  2015cites this paper
• IC3 software model checking on control flow automata

  2015cites this paper
• Memory Management Test-Case Generation of C Programs Using Bounded Model Checking

  2015cites this paper
• Automated Verification of Critical Systems ( AVoCS 2015 ) Studying Verification Conditions for Imperative Programs

  2015cites this paper
• Sound input filter generation for integer overflow errors

  2014cites this paper
• Exploiting Trade-offs in Symbolic Execution for Identifying Security Bugs

  2014influential citation
• Abstraction Recovery for Scalable Static Binary Analysis

  2014influential citation
• Enhancing symbolic execution with veritesting

  2014cites this paper
• The idea is to identify security-critical software bugs so they can be fixed first.

  2014cites this paper
• SPEEDY: An Eclipse-based IDE for invariant inference

  2014cites this paper
• Automatic exploit generation

  2014cites this paper
• OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

  2014cites this paper
• An overview of the Leon verification system: verification by translation to recursive functions

  2013cites this paper
• Joogie: from Java through Jimple to Boogie

  2013cites this paper
• Reflections on Verifying Software with Whiley

  2013cites this paper