Frama-C

swMATH4626MaRDI QIDQ16797FDOQ16797

Author name not available (Why is that?)

Official website: https://frama-c.com/

Source code repository: https://git.frama-c.com/pub/frama-c/

Cited In (59)

• A rewriting logic semantics approach to modular program analysis
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• 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
• Mostly sound type system improves a foundational program verifier
• Towards ``mouldable code via nested code graph transformation
• Formal analysis of the compact position reporting algorithm
• Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method 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
• Automating theorem proving with SMT
• Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
• Deductive verification of floating-point Java programs in KeY
• Static analysis of communicating processes using symbolic transducers
• Formal proof of SCHUR conjugate function
• Viper: a verification infrastructure for permission-based reasoning
• Region analysis for deductive verification of C programs
• Expressing polymorphic types in a many-sorted language
• CRADLE
• 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
• Partitioned memory models for program analysis
• ACSL
• Caduceus
• JML
• Why3
• Spec#
• Verification conditions for source-level imperative programs
• CalcCheck
• WhyML
• PAGAI
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Liveness-driven random program generation
• LCLint
• OpenJML
• Checkmate
• DarwinSPL
• DeltaEcore
• JOANA
• SCCharts
• SCEst
• StaDy
• A survey of satisfiability modulo theory
• Exploiting pointer analysis in memory models for deductive verification
• A relational shape abstract domain
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Leveraging compiler intermediate representation for multi- and cross-language verification
• Multi-prover verification of floating-point programs
• One logic to use them all
• Abstraction and subsumption in modular verification of C programs
• Mechanized semantics for the clight subset of the C language
• Verification of the ROS NavFn planner using executable specification languages
• Integrated approach to analysis and verification of imperative programs

This page was built for software: Frama-C