Frama-C

swMATH4626MaRDI QIDQ16797FDOQ16797

Author name not available (Why is that?)

Cited In (41)

• Cut branches before looking for bugs: certifiably sound verification on relaxed slices
• Verifying Whiley programs with Boogie
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Towards ``mouldable code via nested code graph transformation
• Formal analysis of the compact position reporting algorithm
• Bridging the Gap: Automatic Verified Abstraction of C
• A validated real function calculus
• Contract-based verification of MATLAB-style matrix programs
• How testing helps to diagnose proof failures
• Deductive verification of floating-point Java programs in KeY
• An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
• Region analysis for deductive verification of C programs
• Mostly Sound Type System Improves a Foundational Program Verifier
• One Logic to Use Them All
• Automating deductive verification for weak-memory programs
• A non-linear arithmetic procedure for control-command software verification
• Polynomial function intervals for floating-point software verification
• Credible autocoding of convex optimization algorithms
• Static Analysis of Communicating Processes Using Symbolic Transducers
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Multi-Prover Verification of Floating-Point Programs
• Title not available (Why is that?)
• Verification conditions for source-level imperative programs
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Liveness-driven random program generation
• Formal Proof of SCHUR Conjugate Function
• Expressing Polymorphic Types in a Many-Sorted Language
• Exploiting pointer analysis in memory models for deductive verification
• A relational shape abstract domain
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
• A Rewriting Logic Semantics Approach to Modular Program Analysis
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Principled Software Development
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Abstraction and subsumption in modular verification of C programs
• Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm
• Partitioned Memory Models for Program Analysis
• Mechanized semantics for the clight subset of the C language
• Verification of the ROS NavFn planner using executable specification languages
• A Survey of Satisfiability Modulo Theory
• Automating Theorem Proving with SMT

This page was built for software: Frama-C