836 research outputs found
Meer vrouwen in de ict, waarom eigenlijk?
Full text linkIct lijkt wel een mannensport. Marieke Huisman en Mariëlle Stoelinga, beiden verbonden aan de Universiteit Twente, pleiten voor meer vrouwen in de techniek
Meer vrouwen in de ict, waarom eigenlijk?
No full textIct lijkt wel een mannensport. Marieke Huisman en Mariëlle Stoelinga, beiden verbonden aan de Universiteit Twente, pleiten voor meer vrouwen in de techniek
Preface
Full text linkThis is a preface of the special issue of the 14th international workshop on Automated Verification of Critical Systems. This workshop covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc.)
VerifyThis – Verification Competition with a Human Factor
Full text linkVerifyThis is a series of competitions that aims to evaluate the current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence it is not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. In this paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange
Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171)
Full text linkThis report documents the program and the outcomes of Dagstuhl Seminar 14171
"Evaluating Software-Verification Systems: Benchmarks and Competitions".
The seminar brought together a large group of current and future competition
organizers and participants, benchmark maintainers, as well as practitioners and researchers interested in the topic. The seminar was conducted as a highly-interactive event, with a wide spectrum of contributions from participants, including talks, tutorials, posters, tool demstrations, hands-on sessions, and a live competition
Principles of Contract Languages (Dagstuhl Seminar 22451)
Full text linkThis report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages". At the seminar, participants discussed the fundamental aspects of software contracts. Topics included the format and expressiveness of contracts, their use cases in software development and analysis, and contract composition and decomposition
Foreword: SAVCBS'09 - Proceedings of the 8th International Workshop on Specification and Verification of Component-Based Systems
Full text linkGeneralizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
No full textMetric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.Team Manuel Mazo J
A Case Study in Class Library Verification: Java's Vector Class
No full text) Marieke Huisman, Bart Jacobs, Joachim van den Berg Computing Science Institute, University of Nijmegen Toernooiveld 1, 6525 ED Nijmegen, The Netherlands fmarieke,bart,[email protected] Abstract. This paper presents a veri cation of an invariant property for the Vector class from Java's standard library. The property says (essentially) that the actual size of a vector is less than or equal to its capacity. This property is maintained by all methods of the Vector class, and it holds for all objects created by the constructors of the Vector class. The veri cation relies on two tools: the proof tool PVS is used for reasoning, and the LOOP tool is used for an automatic translation of Java into PVS. This project shows the feasibility of tool-assisted verification for non-trivial Java classes. 1 Introduction One of the reasons for the popularity of object-oriented programming is the possibility it o ers for reuse of code. Usually, the distribution of an object-oriented programming langua..
- …
