Frama-C
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Dafny
- KeY-C
- ROSMonitoring
- Marathon 2
- Whiley
- COMBINE
- KRAKATOA
- How testing helps to diagnose proof failures
- ACSL
- Why3
- Liveness-driven random program generation
- JML
- Spec#
- Caduceus
- Gappa
- cvc3
- Alt-Ergo
- Rascal
- Understanding parameters of deductive verification: an empirical investigation of KeY
- VCC
- SANTE
- PathCrawler
- A validated real function calculus
- PROMELA
- Chalice
- VeriFast
- Boogie
- Formal analysis of the compact position reporting algorithm
- A relational shape abstract domain
- PolyPaver
- TRX
- Verifying Whiley programs with Boogie
- Abstraction and subsumption in modular verification of C programs
- PlusCal
- WhyML
- CalcCheck
- VeriSmall
- KeY
- Region analysis for deductive verification of C programs
- Deductive verification of floating-point Java programs in KeY
- Exploiting pointer analysis in memory models for deductive verification
- VerCors
- Automating deductive verification for weak-memory programs
- A non-linear arithmetic procedure for control-command software verification
- Credible autocoding of convex optimization algorithms
- PAGAI
- RATH-Agda
- Grasshopper
- Joogie
- Mechanized semantics for the clight subset of the C language
- Viper
- Verification of the ROS NavFn planner using executable specification languages
- Viper: a verification infrastructure for permission-based reasoning
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Contract-based verification of MATLAB-style matrix programs
- A survey of satisfiability modulo theory
- NAT2TEST
- Bridging the Gap: Automatic Verified Abstraction of C
- Mostly sound type system improves a foundational program verifier
- Static analysis of communicating processes using symbolic transducers
- Partitioned memory models for program analysis
- Integrated approach to analysis and verification of imperative programs
- LCLint
- coreStar
- JavaSMT
- Atoment
- Java Jr
- SPHIN
- OpenJML
- Expressing polymorphic types in a many-sorted language
- webLurch
- Markdown
- C-Light
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- OSMOSE
- Verdi
- Jessie
- Charge!
- DyTa
- SMACK
- Formal proof of SCHUR conjugate function
- DeltaJ
- JBMC
- StaDy
- CIL
- AstraVer
- Checkmate
- JOANA
- SCCharts
- SCEst
- DarwinSPL
- DeltaEcore
- miTLS
- VST-Floyd
- BINSEC/SE
- Csmith
- ACVS
- Plum Hall
- jsfunfuzz
- SPL Conqueror
This page was built for software: Frama-C
