Cited in
(only showing first 100 items - show all)- An assertional proof of the stability and correctness of Natural Mergesort
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Verifying relative safety, accuracy, and termination for program approximations
- Heaps and Data Structures: A Challenge for Automated Provers
- Inferring Loop Invariants Using Postconditions
- Proving mutual termination
- Verifying Whiley programs with Boogie
- Regression verification for unbalanced recursive functions
- Checking data-race freedom of GPU kernels, compositionally
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Verified cryptographic code for everybody
- Using History Invariants to Verify Observers
- Considerate reasoning and the Composite design pattern
- Faster and more complete extended static checking for the Java modeling language
- The dynamic frames theory
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Safe functional systems through integrity types and verified assembly
- Wombit: a portfolio bit-vector solver using word-level propagation
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Modular verification of procedure equivalence in the presence of memory allocation
- Automating Induction with an SMT Solver
- On Bounded Reachability of Programs with Set Comprehensions
- Splitting via Interpolants
- scientific article; zbMATH DE number 6712238 (Why is no real title available?)
- Beyond contracts for concurrency
- Automated verification of practical garbage collectors
- Contract-based verification of MATLAB-style matrix programs
- Predicate abstraction in a program logic calculus
- Proving the safety of highly-available distributed objects
- Automatic verification of Java programs with dynamic frames
- Alloy*: a general-purpose higher-order relational constraint solver
- Program verification by coinduction
- Deductive verification of floating-point Java programs in KeY
- Two for the price of one: lifting separation logic assertions
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- Conjunctive abstract interpretation using paramodulation
- The relationship between separation logic and implicit dynamic frames
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Fifty years of Hoare's logic
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
- Output-sensitive information flow analysis
- Matching multiplications in bit-vector formulas
- A framework for the verification of certifying computations
- Horn clause solvers for program verification
- A Basis for Verifying Multi-threaded Programs
- Viper: a verification infrastructure for permission-based reasoning
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Assertion-based slicing and slice graphs
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Verification of object-oriented programs: a transformational approach
- Two-level mixed verification method of C-light programs in terms of safety logic
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Shape analysis of low-level C with overlapping structures
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Automating deductive verification for weak-memory programs
- Mechanical inference of invariants for FOR-loops
- Time bounds for general function pointers
- Instrumenting a weakest precondition calculus for counterexample generation
- Loop invariants: analysis, classification, and examples
- Combining model checking and testing
- Automating regression verification of pointer programs by predicate abstraction
- Behavioral interface specification languages
- Boolector
- Dafny
- HOL-Boogie
- KeY-C
- ALGOL 68
- Modula
- IMP++
- CalFuzzer
- SCOOP
- ANTLR
- HOL-Z
- KRAKATOA
- SPARK
- Eiffel
- ACSL
- SMT-LIB
- Daikon
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- cvc3
- Spec#
- LLVM
- Dagger
- SIMPLIFY
- z3
- ProMoVer
- Atelier B
- Rodin
- ESC/Java
- ESC4
- Scala
- PathCrawler
This page was built for software: Boogie
