Cargando…
Deductive Verification of Floating-Point Java Programs in KeY
Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the pre...
Autores principales: | Abbasi, Rosa, Schiffl, Jonas, Darulova, Eva, Ulbrich, Mattias, Ahrendt, Wolfgang |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2021
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984528/ http://dx.doi.org/10.1007/978-3-030-72013-1_13 |
Ejemplares similares
-
A Two-Phase Approach for Conditional Floating-Point Verification
por: Lohar, Debasmita, et al.
Publicado: (2021) -
An Automated Deductive Verification Framework for Circuit-building Quantum Programs
por: Chareton, Christophe, et al.
Publicado: (2021) -
Formal verification of Simulink/Stateflow diagrams: a deductive approach
por: Zhan, Naijun, et al.
Publicado: (2017) -
Formal verification of floating-point hardware design: a mathematical approach
por: Russinoff, David M, et al.
Publicado: (2018) -
Carbon range verification with 718 keV Compton imaging
por: Parajuli, Raj Kumar, et al.
Publicado: (2021)