Avoiding exponential explosion

DOI10.1145/360204.360220zbMath1323.68372OpenAlexW1992431017MaRDI QIDQ5178883

Cormac Flanagan, James B. Saxe

Publication date: 17 March 2015

Published in: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/360204.360220

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Improving Generalization in Software IC3 ⋮ Efficient weakest preconditions ⋮ Generation of correctness conditions for imperative programs ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Certified verification of relational properties ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ Assertion-based slicing and slice graphs ⋮ Symbolic encoding of LL(1) parsing and its applications ⋮ Doomed program points ⋮ Automated verification of functional correctness of race-free GPU programs ⋮ Function extraction ⋮ Unnamed Item ⋮ Verification conditions for source-level imperative programs ⋮ Quantitative information flow as safety and liveness hyperproperties ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Modular verification of multithreaded programs ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Computing Preconditions and Postconditions of While Loops

This page was built for publication: Avoiding exponential explosion