Výsledky vyhledávání - "Claire Dross"

Autor: Claire Dross

Publikováno v: ACM SIGAda Ada Letters. 42:62-68

The SPARK tool analyzes Ada programs statically. It can be used to verify both that a program is free from runtime exceptions and that it conforms to a specification expressed through contracts. To facilitate dynamic analysis, Ada contracts are regul

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e02be15d5054243b3747637bd2c56034
https://doi.org/10.1145/3591335.3591341

Zobrazit plný text záznamu

Proving the Correctness of GNAT Light Runtime Library

Autor: Yannick Moy, Claire Dross

Publikováno v: ACM SIGAda Ada Letters. 42:65-67

The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use at the highest levels of criticality in several industrial domains. It contains around 180 units foc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9b3ce2918aac58a5aeace75886878065
https://doi.org/10.1145/3577949.3577959

Zobrazit plný text záznamu

VerifyThis 2019: a program verification competition

Autor: Claire Dross, Carlo A Furia, Marieke Huisman, Rosemary Monahan, Peter Müller

Publikováno v: International journal on software tools for technology transfer, 23(6), 883-893. Springer
International Journal on Software Tools for Technology Transfer, 23

International Journal on Software Tools for Technology Transfer, 23
ISSN:1433-2779
ISSN:1433-2787

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3e5dd550346389517576552d64ec4742
https://doi.org/10.1007/s10009-021-00619-x

Zobrazit plný text záznamu

Making Proofs of Floating-Point Programs Accessible to Regular Developers

Autor: Claire Dross, Johannes Kanig

Publikováno v: Lecture Notes in Computer Science ISBN: 9783030955601

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::ecf3db9d8a61c7e34b0ac6a8af3f80e7
https://doi.org/10.1007/978-3-030-95561-8_2

Zobrazit plný text záznamu

Defining a Pattern Matching Language Feature for Ada

Autor: S. Tucker Taft, Stephen Baird, Claire Dross

Publikováno v: ACM SIGAda Ada Letters. 42:79-79

Structural pattern-matching as a language feature has become more common in programming languages over the past decade. This talk will report on the work in progress to define such a feature for the Ada language, both from a language-design point of

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9cf46ad4eeb1578c7ea9a800ec2d656e
https://doi.org/10.1145/3577949.3577963

Zobrazit plný text záznamu

Recursive Data Structures in SPARK

Autor: Johannes Kanig, Claire Dross

Publikováno v: Computer Aided Verification ISBN: 9783030532901
CAV (2)

SPARK is both a deductive verification tool for the Ada language and the subset of Ada on which it operates. In this paper, we present a recent extension of the SPARK language and toolset to support pointers. This extension is based on an ownership p

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::79ac3f1ffb44719ff02bd5e97df05d3a
https://doi.org/10.1007/978-3-030-53291-8_11

Zobrazit plný text záznamu

Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK

Autor: Yannick Moy, Claire Dross, Benjamin M. Brosgol

Publikováno v: SecDev

This hands-on tutorial will show attendees how to use formal methods in developing and verifying high-assurance software. It will cover the benefits and costs of formal methods technology, describe its capabilities and limits, summarize how to adopt

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::861de3f04159b2d930533717f6d43cd3
https://doi.org/10.1109/secdev.2019.00012

Zobrazit plný text záznamu

Practical Application of SPARK to OpenUxAS

Autor: M. Anthony Aiello, Laura Humphrey, James Hamil, Patrick Rogers, Claire Dross

Publikováno v: Lecture Notes in Computer Science ISBN: 9783030309411
FM

This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::322394c6e432c3665490d2948cdf4b03
https://doi.org/10.1007/978-3-030-30942-8_45

Zobrazit plný text záznamu

Teaching Deductive Verification Through Frama-C and SPARK for Non Computer Scientists

Autor: Léo Creuse, Christophe Garion, Jérôme Hugues, Joffrey Huguet, Claire Dross

Publikováno v: Formal Methods Teaching ISBN: 9783030324407
FMTea

Deductive verification of software is a formal method that is usually taught in Computer Science curriculum. But how can students with no strong background in Computer Science be exposed to such a technique? We present in this paper two experiments m

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::62de6482f116a7f746a9660a27dc9848
https://oatao.univ-toulouse.fr/25174/

Zobrazit plný text záznamu

Reasoning with Triggers

Autor: Johannes Kanig, Sylvain Conchon, Claire Dross, Andrei Paskevich

Publikováno v: EPiC Series in Computing.

SMT solvers can decide the satisfiability of ground formulas modulo a combination ofbuilt-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e79eb2ca596b8f92ca571dbcbbbf292e
https://doi.org/10.29007/3c1n

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání