KRAKATOA

swMATH3159MaRDI QIDQ15691FDOQ15691

Author name not available (Why is that?)

Official website: http://krakatoa.lri.fr/

Cited In (98)

• Title not available (Why is that?)
• Formal verification of side-channel countermeasures using self-composition
• Algebraic Methodology and Software Technology
• LCF-style Platform based on Multiway Decision Graphs
• Deductive verification of floating-point Java programs in KeY
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Reasoning about assignments in recursive data structures
• ZB 2005: Formal Specification and Development in Z and B
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Exploiting pointer analysis in memory models for deductive verification
• Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender
• Verification of Java Programs with Generics
• Practical Tactics for Separation Logic
• An Introduction to Certificate Translation
• A refinement methodology for object-oriented programs
• Semi-persistent Data Structures
• Theorem Proving in Higher Order Logics
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• 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
• Imperative Functional Programming with Isabelle/HOL
• Product programs in the wild: retrofitting program verifiers to check information flow security
• 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
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• 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
• Fundamental Approaches to Software Engineering
• Matching logic: an alternative to Hoare/Floyd logic
• 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
• Complete instantiation-based interpolation
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Modular inference of subprogram contracts for safety checking
• Instrumenting a weakest precondition calculus for counterexample generation
• Behavioral interface specification languages
• Static contract checking with abstract interpretation
• HOL-Boogie
• A verifying compiler for a multi-threaded object-oriented language
• ACSL
• Caduceus
• JML
• Frama-C
• Omnibus
• Why3
• Spec#
• Theorem Proving in Higher Order Logics
• Verification conditions for source-level imperative programs
• A dynamic logic for deductive verification of multi-threaded programs
• MARMOT
• HighSpec
• WhyML
• VeriCool
• ASTREE
• Octagon
• Haskabelle
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Correct code containing containers
• Splint
• OpenJML
• Cibai
• Specification and runtime verification of Java card programs
• JCML: A specification language for the runtime verification of Java card programs
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• ANNA
• Local reasoning for global invariants. II: Dynamic boundaries
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Weakest pre-condition reasoning for Java programs with JML annotations
• Doomed program points
• Reasoning about memory layouts
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• A system for compositional verification of asynchronous objects
• CPBPV: a constraint-programming framework for bounded program verification
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Multi-prover verification of floating-point programs
• One logic to use them all
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Specification and verification challenges for sequential object-oriented programs
• Practical realisation and elimination of an ECC-related software bug attack
• Proving fairness and implementation correctness of a microkernel scheduler
• A proof outline logic for object-oriented programming
• Dafny: an automatic program verifier for functional correctness
• MUNCH -- automated reasoner for sets and multisets
• A dynamic logic for unstructured programs with embedded assertions
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• TASS: the toolkit for accurate scientific software
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• A Hoare Logic for Call-by-Value Functional Programs

This page was built for software: KRAKATOA