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