CoVeriTeam: On-Demand Composition of Cooperative Verification Systems

Autor: Dirk Beyer, Sudeep Kanav

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232

There is no silver bullet for software verification: Different techniques have different strengths. Thus, it is imperative to combine the strengths of verification tools via combinations and cooperation. CoVeriTeam is a language and tool for on-deman

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::54d255e76c30d754066727ef237fec96
https://doi.org/10.1007/978-3-030-99524-9_31

An Interface Theory for Program Verification

Autor: Sudeep Kanav, Dirk Beyer

Publikováno v: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles ISBN: 9783030613617
ISoLA (1)

Program verification is the problem, for a given program $$P$$and a specification $$\phi $$, of constructing a proof of correctness for the statement “program $$P$$satisfies specification $$\phi $$” ($$P \models \phi $$) or a proof of violation (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::8e14f6d3de0eb4d6ae5f84e5285e8c5e
https://doi.org/10.1007/978-3-030-61362-4_9

Tool Support for Live Formal Verification

Autor: Sudeep Kanav, Vincent Aravantinos

Publikováno v: MoDELS

Despite an increasing interest from industry (e.g., DO333 standard [1]), formal verification is still not widely used in production for safety critical systems. This has been recognized for a while and various causes have been identified, one of them

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::ce81b3b031f2484017c367c2c2e57789
https://doi.org/10.1109/models.2017.6

A Conference Management System with Verified Document Confidentiality

Autor: Sudeep Kanav, Andrei Popescu, Peter Lammich

Publikováno v: Computer Aided Verification ISBN: 9783319088662
CAV
Kanav, S, Lammich, P & Popescu, A 2014, A Conference Management System with Verified Document Confidentiality . in International Conference on Computer Aided Verification . Computer Aided Verification, vol. 8559, pp. 167-183 . https://doi.org/10.1007/978-3-319-08867-9_11

We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality pr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::87a2baa9e8a472733b2c754d118e4617
https://doi.org/10.1007/978-3-319-08867-9_11