Cited in
(only showing first 100 items - show all)- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Verification, Model Checking, and Abstract Interpretation
- Inferring Loop Invariants Using Postconditions
- Verifying Whiley programs with Boogie
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Imperative Functional Programming with Isabelle/HOL
- scientific article; zbMATH DE number 7566072 (Why is no real title available?)
- Formal verification of side-channel countermeasures using self-composition
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automating Induction with an SMT Solver
- A Certified Lightweight Non-interference Java Bytecode Verifier
- Algebraic Methodology and Software Technology
- Deductive verification of floating-point Java programs in KeY
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- LCF-style Platform based on Multiway Decision Graphs
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A framework for the verification of certifying computations
- Viper: a verification infrastructure for permission-based reasoning
- Matching logic: an alternative to Hoare/Floyd logic
- Fundamental Approaches to Software Engineering
- Automatic decidability and combinability
- A program logic for resources
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- Typed Lambda Calculi and Applications
- Hardware-Dependent Proofs of Numerical Programs
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Complete instantiation-based interpolation
- Modular inference of subprogram contracts for safety checking
- Instrumenting a weakest precondition calculus for counterexample generation
- Reasoning about assignments in recursive data structures
- Behavioral interface specification languages
- Grail
- HOL-Boogie
- KeY-C
- LARCH
- TVOC
- SPARK
- Eiffel
- ACSL
- Daikon
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- Gappa
- ISP
- Spec#
- SIMPLIFY
- TASS_
- JCML
- ESC/Java
- MUNCH
- JUnit
- SANTE
- VCC
- JACK
- Boogie
- Chalice
- VeriFast
- MARMOT
- HighSpec
- KeY
- SLAB
- KIV
- WhyML
- VeriCool
- LOOP
- jStar
- MDGs
- Jahob
- Traffic 4
- ASTREE
- Grasshopper
- Octagon
- BVD
- Haskabelle
- Grail
- coreStar
- Splint
- Houdini
- OpenJML
- BoogiePL
- Jessie
- ASMKeY
- AstraVer
- Cibai
- Camelot
- SPL Conqueror
- Maximum Cardinality Matching
- AutoProof
- Jass
- ShortestPath
- SCiFI
- STLlint
- ANNA
- Nagini
This page was built for software: KRAKATOA
