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 (only showing first 100 items - show all)
- A rewriting logic semantics approach to modular program analysis
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Towards ``mouldable code via nested code graph transformation
- Bridging the Gap: Automatic Verified Abstraction of C
- A validated real function calculus
- Contract-based verification of MATLAB-style matrix programs
- Polynomial function intervals for floating-point software verification
- Credible autocoding of convex optimization algorithms
- Dafny
- KeY-C
- Partitioned memory models for program analysis
- COMBINE
- KRAKATOA
- ACSL
- Caduceus
- JML
- Why3
- Alt-Ergo
- cvc3
- Gappa
- Spec#
- Rascal
- PathCrawler
- SANTE
- VCC
- Boogie
- Chalice
- PROMELA
- VeriFast
- PolyPaver
- TRX
- PlusCal
- CalcCheck
- KeY
- WhyML
- VeriSmall
- Viper
- VerCors
- PAGAI
- RATH-Agda
- Grasshopper
- Joogie
- NAT2TEST
- coreStar
- LCLint
- JavaSMT
- Atoment
- Java Jr
- OpenJML
- SPHIN
- C-Light
- Markdown
- OSMOSE
- webLurch
- Charge!
- Verdi
- Jessie
- DyTa
- SMACK
- DeltaJ
- JBMC
- CIL
- AstraVer
- Checkmate
- DarwinSPL
- DeltaEcore
- JOANA
- SCCharts
- SCEst
- StaDy
- miTLS
- BINSEC/SE
- ACVS
- Csmith
- jsfunfuzz
- EPGY
- Plum Hall
- VST-Floyd
- SPL Conqueror
- Calysto
- RVT
- C-to-Isabelle
- SILF
- Cascade
- Crust
- GraVy
- A survey of satisfiability modulo theory
- PRECiSA
- RangeLab
- Daisy
- KeYmaera X
- Nagini
- QF_FP
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- Multi-prover verification of floating-point programs
- One logic to use them all
- Mechanized semantics for the clight subset of the C language
- 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
This page was built for software: Frama-C
