Volume
OASIcs, Volume 24
6th International Workshop on Systems Software Verification
- Part of: Series: Open Access Series in Informatics (OASIcs)
Event
SSV 2011, August 26, 2011, Nijmegen, The NetherlandsEditors
Publication Details
- published at: 2012-07-13
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-36-1
- DBLP: db/conf/ssv/ssv2011
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 24, SSV'11, Complete Volume
Abstract
OASIcs, Volume 24, SSV'11, Complete Volume
Cite as
6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@Proceedings{brauer_et_al:OASIcs.SSV.2011,
title = {{OASIcs, Volume 24, SSV'11, Complete Volume}},
booktitle = {6th International Workshop on Systems Software Verification},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011},
URN = {urn:nbn:de:0030-drops-35937},
doi = {10.4230/OASIcs.SSV.2011},
annote = {Keywords: Software/Program Verification}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface
Abstract
Frontmatter, Table of Contents, Preface
Cite as
6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. i-vii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{brauer_et_al:OASIcs.SSV.2011.i,
author = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
title = {{Frontmatter, Table of Contents, Preface}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {i--vii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.i},
URN = {urn:nbn:de:0030-drops-35854},
doi = {10.4230/OASIcs.SSV.2011.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface}
}
Document
Structuring Interactive Correctness Proofs by Formalizing Coding Idioms
Abstract
This paper examines a novel strategy for developing correctness proofs in interactive software verification for C programs. Rather than proceeding backwards from the generated verification conditions, we start by developing a library of the employed data structures and related coding idioms. The application of that library then leads to correctness proofs that reflect informal arguments about the idioms. We apply this strategy to the low-level memory allocator of the L4 microkernel, a case study discussed in the literature.
Cite as
Holger Gast. Structuring Interactive Correctness Proofs by Formalizing Coding Idioms. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{gast:OASIcs.SSV.2011.1,
author = {Gast, Holger},
title = {{Structuring Interactive Correctness Proofs by Formalizing Coding Idioms}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {1--14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.1},
URN = {urn:nbn:de:0030-drops-35864},
doi = {10.4230/OASIcs.SSV.2011.1},
annote = {Keywords: software verification, coding idioms, theory re-use, low-level code}
}
Document
Verification of Dependable Software using SPARK and Isabelle
Abstract
We present a link between the interactive proof assistant Isabelle/HOL and the SPARK/Ada tool suite for the verification of high-integrity software. Using this link, we can tackle verification
problems that are beyond reach of the proof tools currently available for Spark. To demonstrate that our methodology is suitable for real-world applications, we show how it can be used to verify
an efficient library for big numbers. This library is then used as a basis for an implementation of the RSA public-key encryption algorithm in SPARK/Ada.
Cite as
Stefan Berghofer. Verification of Dependable Software using SPARK and Isabelle. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 15-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{berghofer:OASIcs.SSV.2011.15,
author = {Berghofer, Stefan},
title = {{Verification of Dependable Software using SPARK and Isabelle}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {15--31},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.15},
URN = {urn:nbn:de:0030-drops-35876},
doi = {10.4230/OASIcs.SSV.2011.15},
annote = {Keywords: Software/Program Verification}
}
Document
Adaptable Value-Set Analysis for Low-Level Code
Abstract
This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties
about medium-sized microcontroller programs.
Cite as
Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{brauer_et_al:OASIcs.SSV.2011.32,
author = {Brauer, J\"{o}rg and Hansen, Ren\'{e} Rydhof and Kowalewski, Stefan and Larsen, Kim G. and Olesen, Mads Chr.},
title = {{Adaptable Value-Set Analysis for Low-Level Code}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {32--43},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32},
URN = {urn:nbn:de:0030-drops-35884},
doi = {10.4230/OASIcs.SSV.2011.32},
annote = {Keywords: Abstract interpretation, SAT solving, embedded systems}
}
Document
Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools
Abstract
paper, we describe a case study where a simple 2oo3 voting scheme for a shutdown system was verified using two bounded model checking tools, CBMC and EBMC. The system represents Systematic Capability level 3 according to IEC 61508 ed2.0. The verification process was based on requirements and pseudo code, and involved verifying C and Verilog code implementing the pseudo code. The results suggest that the tools were suitable for the task, but require considerable
training to reach productive use for code embedded in industrial equipment. We also identified some issues in the development process that could be streamlined with the use of more formal verification methods. Towards the end of the paper, we discuss the issues we found and how to address them in a practical setting.
Cite as
Antti Jääskeläinen, Mika Katara, Shmuel Katz, and Heikki Virtanen. Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 44-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{jaaskelainen_et_al:OASIcs.SSV.2011.44,
author = {J\"{a}\"{a}skel\"{a}inen, Antti and Katara, Mika and Katz, Shmuel and Virtanen, Heikki},
title = {{Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {44--56},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.44},
URN = {urn:nbn:de:0030-drops-35891},
doi = {10.4230/OASIcs.SSV.2011.44},
annote = {Keywords: Functional safety, SIL-3, model checking, tools}
}
Document
A Tool for the Certification of Sequential Function Chart based System Specifications
Abstract
We describe a tool framework for certifying properties of sequential function chart (SFC)based system specifications: CertPLC. CertPLC handles programmable logic controller (PLC) descriptions provided in the SFC language of the IEC 61131–3 standard. It provides routines to
certify properties of systems by delivering an independently checkable formal system description and proof (called certificate) for the desired properties. We focus on properties that can be
described as inductive invariants. System descriptions and certificates are generated and handled using the Coq proof assistant. Our tool framework is used to provide supporting evidence for the safety of embedded systems in the industrial automation domain to third-party authorities. In this paper we focus on the tool's architecture, requirements and implementation aspects.
Cite as
Jan Olaf Blech. A Tool for the Certification of Sequential Function Chart based System Specifications. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 57-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{blech:OASIcs.SSV.2011.57,
author = {Blech, Jan Olaf},
title = {{A Tool for the Certification of Sequential Function Chart based System Specifications}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {57--70},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.57},
URN = {urn:nbn:de:0030-drops-35904},
doi = {10.4230/OASIcs.SSV.2011.57},
annote = {Keywords: Software/Program Verification}
}
Document
Automatic Derivation of Abstract Semantics From Instruction Set Descriptions
Abstract
Abstracted semantics of instructions of processor-based architectures are an invaluable asset for several formal verification techniques, such as software model checking and static analysis. In the field of model checking, abstract versions of instructions can help counter the state explosion problem, for instance by replacing explicit values by symbolic representations of sets of values. Similar to this, static analyses often operate on an abstract domain in order to reduce complexity, guarantee termination, or both. Hence, for a given microcontroller, the task at hand is to find such abstractions. Due to the large number of available microcontrollers, some of which are even created for specific applications, it is impracticable to rely on human developers to perform this step. Therefore, we propose a technique that starts from imperative descriptions of instructions,
which allows to automate most of the process.
Cite as
Dominique Gückel and Stefan Kowalewski. Automatic Derivation of Abstract Semantics From Instruction Set Descriptions. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 71-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
Copy BibTex To Clipboard
@InProceedings{guckel_et_al:OASIcs.SSV.2011.71,
author = {G\"{u}ckel, Dominique and Kowalewski, Stefan},
title = {{Automatic Derivation of Abstract Semantics From Instruction Set Descriptions}},
booktitle = {6th International Workshop on Systems Software Verification},
pages = {71--83},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-36-1},
ISSN = {2190-6807},
year = {2012},
volume = {24},
editor = {Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.71},
URN = {urn:nbn:de:0030-drops-35919},
doi = {10.4230/OASIcs.SSV.2011.71},
annote = {Keywords: Model Checking, Static Analysis, Hardware Description Languages}
}