Cited in
(only showing first 100 items - show all)- Crust
- GraVy
- PRECiSA
- RangeLab
- Daisy
- KeYmaera X
- Nagini
- QF_FP
- Credible autocoding of convex optimization algorithms
- Verification conditions for source-level imperative programs
- Partitioned memory models for program analysis
- Understanding parameters of deductive verification: an empirical investigation of KeY
- Liveness-driven random program generation
- 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
- Marathon 2
- ROSMonitoring
- Whiley
- Abstraction and subsumption in modular verification of C programs
- One logic to use them all
- Multi-prover verification of floating-point 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
- JMLAutoTest
- RustBelt
- Whiteoak
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- A rewriting logic semantics approach to modular program analysis
- 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
- CRADLE
- Formal analysis of the compact position reporting algorithm
- A validated real function calculus
- Bridging the Gap: Automatic Verified Abstraction of C
- Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method algorithm
- Contract-based verification of MATLAB-style matrix programs
- How testing helps to diagnose proof failures
- Deductive verification of floating-point Java programs in KeY
- 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
- 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
- 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
- Dafny
- KeY-C
- 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
This page was built for software: Frama-C
