Verification of Certifying Computations through AutoCorres and Simpl (English)
- New search for: Noschinski, Lars
- New search for: Rizkallah, Christine
- New search for: Mehlhorn, Kurt
- New search for: Noschinski, Lars
- New search for: Rizkallah, Christine
- New search for: Mehlhorn, Kurt
In:
NFM, NASA Formal Methods International Symposium, 6
;
46-61
;
2014
-
ISSN:
- Conference paper / Print
-
Title:Verification of Certifying Computations through AutoCorres and Simpl
-
Contributors:
-
Published in:Lecture Notes in Computer Science ; 8430 ; 46-61
-
Publisher:
- New search for: Springer International Publishing
-
Place of publication:Cham
-
Publication date:2014
-
Size:16 Seiten
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Conference paper
-
Type of material:Print
-
Language:English
-
Keywords:
-
Source:
Table of contents conference proceedings
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
DO-333 Certification Case StudiesCofer, D. / Miller, S. et al. | 2014
- 16
-
A Compositional Monitoring Framework for Hard Real-Time Systemsde Matos Pedro, A. / Pereira, D. / Pinho, L.M. / Pinto, J.S. et al. | 2014
- 31
-
Leadership Election: An Industrial SoS Application of Compositional Deadlock VerificationAntonino, P.R.G. / Oliveira, M.M. / Sampaio, A.C.A. / Kristensen, K.E. / Bryans, J.W. et al. | 2014
- 46
-
Verification of Certifying Computations through AutoCorres and SimplNoschinski, L. / Rizkallah, C. / Mehlhorn, K. et al. | 2014
- 62
-
Distinguishing Sequences for Partially Specified FSMsHierons, R.M. / Turker, U.C. et al. | 2014
- 77
-
On Proving Recoverability of Smart Electrical GridsHorsmanheimo, S. / Kamali, M. / Kolehmainen, M. / Neovius, M. / Petre, L. / Ronkko, M. / Sandvik, P. et al. | 2014
- 92
-
Providing Early Warnings of Specification ProblemsHoffman, D. / Tagore, A. / Zaccai, D. / Weide, B.W. et al. | 2014
- 98
-
Mechanized, Compositional Verification of Low-Level CodeBartels, B. / Jahnig, N. et al. | 2014
- 113
-
Formally Verified Computation of Enclosures of Solutions of Ordinary Differential EquationsImmler, F. et al. | 2014
- 128
-
On the Quantum Formalization of Coherent Light in HOLMahmoud, M.Y. / Tahar, S. et al. | 2014
- 143
-
Refinement Types for TLA+Merz, S. / Vanzetto, H. et al. | 2014
- 158
-
Using Lightweight Theorem Proving in an Asynchronous Systems ContextDanish, M. / Xi, H. et al. | 2014
- 173
-
JKelloy: A Proof Assistant for Relational Specifications of Java ProgramsEl Ghazi, A.A. / Ulbrich, M. / Gladisch, C. / Tyszberowicz, S. / Taghdiri, M. et al. | 2014
- 188
-
Verifying Hybrid Systems Involving Transcendental FunctionsJackson, P. / Sogokon, A. / Bridge, J. / Paulson, L. et al. | 2014
- 203
-
Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem ProvingDenman, W. et al. | 2014
- 209
-
Combining PVSio with StateflowMasci, P. / Zhang, Y. / Jones, P. / Oladimeji, P. / D Urso, E. / Bernardeschi, C. / Curzon, P. / Thimbleby, H. et al. | 2014
- 215
-
Qed. Computing What Remains to Be ProvedCorrenson, L. et al. | 2014
- 230
-
Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU KernelsBardsley, E. / Donaldson, A.F. et al. | 2014
- 246
-
Testing-Based Compiler Validation for Synchronous LanguagesGaroche, P.-L. / Howar, F. / Kahsai, T. / Thirioux, X. et al. | 2014
- 252
-
Automated Testcase Generation for Numerical Support Functions in Embedded SystemsSchumann, J. / Schneider, S.-A. et al. | 2014
- 258
-
REFINER: Towards Formal Verification of Model TransformationsWijs, A. / Engelen, L. et al. | 2014
- 264
-
Designing a Deadlock-Free Train Scheduler: A Model Checking ApproachMazzanti, F. / Spagnolo, G.O. / Ferrari, A. et al. | 2014
- 270
-
A Synthesized Algorithm for Interactive ConsistencyGascon, A. / Tiwari, A. et al. | 2014
- 285
-
Energy-Utility QuantilesBaier, C. / Daum, M. / Dubslaff, C. / Klein, J. / Kluppelholz, S. et al. | 2014
- 300
-
Incremental Verification of Compiler OptimizationsFedyukovich, G. / Gurfinkel, A. / Sharygina, N. et al. | 2014
- 307
-
Memory Efficient Data Structures for Explicit Verification of Timed SystemsJensen, P.G. / Larsen, K.G. / Srba, J. / Sorensen, M.G. / Taankvist, J.H. et al. | 2014
- 313
-
The Gradual VerifierArlt, S. / Rubio-Gonzalez, C. / Rummer, P. / Schaf, M. / Shankar, N. et al. | 2014
- 328
-
Synthesizing Predicates from Abstract Domain LossesMihaila, B. / Simon, A. et al. | 2014
- 343
-
Formal Verification of kLIBC with the WP Frama-C Plug-inCarvalho, N. / da Silva Sousa, C. / Pinto, J.S. / Tomb, A. et al. | 2014