Deductive verification of floating-point Java programs in KeY
From MaRDI portal
Publication:2233510
DOI10.1007/978-3-030-72013-1_13zbMath1474.68186arXiv2101.08733OpenAlexW3146695734MaRDI QIDQ2233510
Wolfgang Ahrendt, Eva Darulova, Rosa Abbasi, Jonas Schiffl, Mattias Ulbrich
Publication date: 18 October 2021
Full work available at URL: https://arxiv.org/abs/2101.08733
Theory of programming languages (68N15) Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- MetiTarski: An automatic theorem prover for real-valued special functions
- A formal analysis of the compact position reporting algorithm
- Automating the verification of floating-point programs
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- A parameterized floating-point formalizaton in HOL Light
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Automatic detection of floating-point exceptions
- Building High Integrity Applications with SPARK
- Static Analysis of Finite Precision Computations
- Certified Roundoff Error Bounds Using Semidefinite Programming
- Handbook of Floating-Point Arithmetic
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Combining Coq and Gappa for Certifying Floating-Point Programs
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
- The MathSAT5 SMT Solver
- Sound compilation of reals
This page was built for publication: Deductive verification of floating-point Java programs in KeY
