Boogie

swMATH7714MaRDI QIDQ19731FDOQ19731

Author name not available (Why is that?)

Official website: http://research.microsoft.com/en-us/projects/boogie/

Source code repository: https://github.com/boogie-org/boogie

Cited In (only showing first 100 items - show all)

• Inferring Loop Invariants Using Postconditions
• Verifying relative safety, accuracy, and termination for program approximations
• Regression verification for unbalanced recursive functions
• Proving mutual termination
• Faster and more complete extended static checking for the Java modeling language
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• The dynamic frames theory
• Wombit: a portfolio bit-vector solver using word-level propagation
• Automating Induction with an SMT Solver
• Automated verification of practical garbage collectors
• Predicate abstraction in a program logic calculus
• Contract-based verification of MATLAB-style matrix programs
• Automatic verification of Java programs with dynamic frames
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Matching multiplications in bit-vector formulas
• A Basis for Verifying Multi-threaded Programs
• A framework for the verification of certifying computations
• Assertion-based slicing and slice graphs
• Verification of object-oriented programs: a transformational approach
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• Mechanical inference of invariants for FOR-loops
• Behavioral interface specification languages
• Static contract checking with abstract interpretation
• Boolector
• HOL-Boogie
• IMP++
• ACSL
• SMT-LIB
• distcc
• Caduceus
• JML
• Frama-C
• Omnibus
• Why3
• Spec#
• Compositionality Entails Sequentializability
• Verification conditions for source-level imperative programs
• cminor
• HighSpec
• InvGen
• FixBag
• WhyML
• VeriCool
• BAP
• GKLEE
• CFML
• SymDiff
• YOGI
• FunArray
• VERL
• DynaMate
• SeaHorn
• OpenJML
• CoVaC
• ACCEPT
• Chisel
• FlexJava
• Cibai
• DarwinSPL
• DeltaEcore
• SCCharts
• SCEst
• Kami
• CoqInE
• CacheAudit
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• Secure distributed programming with value-dependent types
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Valigator: A Verification Tool with Bound and Invariant Generation
• ANNA
• Doomed program points
• Reasoning about memory layouts
• A system for compositional verification of asynchronous objects
• An extensible encoding of object-oriented data models in HOL. With an application to IMP++
• SMT proof checking using a logical framework
• Specification and verification challenges for sequential object-oriented programs
• Magic-sets for localised analysis of Java bytecode
• Proving fairness and implementation correctness of a microkernel scheduler
• Predicate Abstraction in a Program Logic Calculus
• Dafny: an automatic program verifier for functional correctness
• Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings
• Why3 -- where programs meet provers
• Zeno: an automated prover for properties of recursive data structures
• Verification of concurrent systems with VerCors
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• SMT-based model checking for recursive programs
• A learning-based approach to synthesizing invariants for incomplete verification engines
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Heaps and Data Structures: A Challenge for Automated Provers
• Using History Invariants to Verify Observers
• Verifying Whiley programs with Boogie
• 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
• Considerate reasoning and the Composite design pattern
• Safe functional systems through integrity types and verified assembly
• Modular verification of procedure equivalence in the presence of memory allocation
• On Bounded Reachability of Programs with Set Comprehensions

This page was built for software: Boogie