Search

Your search keyword '"Huisman, Marieke"' showing total 106 results
Start Over Author "Huisman, Marieke" Publication Year Range Last 3 years

Refine your results

more »

more »

more »
106 results on '"Huisman, Marieke"'

1. HaliVer: Deductive Verification and Scheduling Languages Join Forces

Author

Haak, Lars B. van den, Wijs, Anton, Huisman, Marieke, and Brand, Mark van den

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages
Abstract

The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses Vercors, a separation logic-based verifier, to verify the correctness of (1) the Halide algorithms and (2) the optimised parallel code produced by \halide when an optimisation schedule is applied to the algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic Halide algorithms, using all but one of the essential scheduling directives available in Halide. Without annotation effort, Haliver proves memory safety in almost all programs. With annotations Haliver, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.

Published
2024

4. The VerCors Verifier: A Progress Report

Author

Armborst, Lukas, Bos, Pieter, van den Haak, Lars B., Huisman, Marieke, Rubbens, Robert, Şakar, Ömer, Tasche, Philip, Goos, Gerhard, Series Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Gurfinkel, Arie, editor, and Ganesh, Vijay, editor

Published
2024
Full Text
View/download PDF

5. First Steps towards Deductive Verification of LLVM IR

Author

van Oorschot, Dré, Huisman, Marieke, Şakar, Ömer, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Beyer, Dirk, editor, and Cavalcanti, Ana, editor

Published
2024
Full Text
View/download PDF

7. Deductive Verification of Parameterized Embedded Systems Modeled in SystemC

Author

Tasche, Philip, Monti, Raúl E., Drerup, Stefanie Eva, Blohm, Pauline, Herber, Paula, Huisman, Marieke, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Dimitrova, Rayna, editor, Lahav, Ori, editor, and Wolff, Sebastian, editor

Published
2024
Full Text
View/download PDF

12. System Modelling

Author

Huisman, Marieke, Wijs, Anton, Hazzan, Orit, Series Editor, Huisman, Marieke, and Wijs, Anton

Published
2023
Full Text
View/download PDF

14. Introduction

Author

Huisman, Marieke, Wijs, Anton, Hazzan, Orit, Series Editor, Huisman, Marieke, and Wijs, Anton

Published
2023
Full Text
View/download PDF

20. JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java

Author

Bliudze, Simon, van den Bos, Petra, Huisman, Marieke, Rubbens, Robert, Safina, Larisa, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Lambers, Leen, editor, and Uchitel, Sebastián, editor

Published
2023
Full Text
View/download PDF

25. SpecifyThis – Bridging Gaps Between Program Specification Paradigms

Author

Ahrendt, Wolfgang, Herber, Paula, Huisman, Marieke, Ulbrich, Mattias, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2022
Full Text
View/download PDF

26. The Integration of Testing and Program Verification : A Position Paper

Author

van den Bos, Petra, Huisman, Marieke, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Jansen, Nils, editor, Stoelinga, Mariëlle, editor, and van den Bos, Petra, editor

Published
2022
Full Text
View/download PDF

27. Teaching Design by Contract Using Snap!

Author

Huisman, Marieke, Monti, Raúl E., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Ahrendt, Wolfgang, editor, Beckert, Bernhard, editor, Bubel, Richard, editor, and Johnsen, Einar Broch, editor

Published
2022
Full Text
View/download PDF

28. Alpinist: An Annotation-Aware GPU Program Optimizer

Author

Şakar, Ömer, Safari, Mohsen, Huisman, Marieke, Wijs, Anton, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Fisman, Dana, editor, and Rosu, Grigore, editor

Published
2022
Full Text
View/download PDF

40. Principles of Contract Languages (Dagstuhl Seminar 22451)

Author

Dilian Gurov and Reiner Hähnle and Marieke Huisman and Giles Reger and Christian Lidström, Gurov, Dilian, Hähnle, Reiner, Huisman, Marieke, Reger, Giles, Lidström, Christian, Dilian Gurov and Reiner Hähnle and Marieke Huisman and Giles Reger and Christian Lidström, Gurov, Dilian, Hähnle, Reiner, Huisman, Marieke, Reger, Giles, and Lidström, Christian

Abstract

This 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.

Published
2023
Full Text
View/download PDF

42. JavaBIP meets VerCors:Towards the Safety of Concurrent Software Systems in Java

Author

Bliudze, Simon, Bos, Petra van den, Huisman, Marieke, Rubbens, Robert, Safina, Larisa, Lambers, Leen, Uchitel, Sebastián, Self-adaptation for distributed services and large software systems [SPIRALS], Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL], Formal Methods and Tools [FMT group], Analyses and Languages Constructs for Object-Oriented Application Evolution [RMOD], Formal Methods and Tools, Digital Society Institute, Self-adaptation for distributed services and large software systems (SPIRALS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Formal Methods and Tools (FMT group), University of Twente, Analyses and Languages Constructs for Object-Oriented Application Evolution (RMOD), ANR-16-IDEX-0004,ULNE,ULNE(2016), ANR-21-CE48-0011,NARCO,Compositions Non-agrégatives de Resources(2021), and Bliudze, Simon

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

We present “Verified JavaBIP”, a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machines, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the “Solidity Casino” case study, known from the VerifyThis Collaborative Long Term Challenge.

Published
2023

43. Principles of Contract Languages (Dagstuhl Seminar 22451)

Author

Gurov, Dilian, Hähnle, Reiner, Huisman, Marieke, Reger, Giles, and Lidström, Christian

Subjects
program analysis, software contracts, software development, Theory of computation → Program specifications, program specifications
Abstract

This 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., DagRep, Volume 12, Issue 11, pages 1-27

Published
2023
Full Text
View/download PDF

44. VerifyThis 2019: a program verification competition

Author

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

Abstract

VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days ofwork. This report analyzes howthe participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

Published
2022

47. The Integration of Testing and Program Verification: A Position Paper

Author

Bos, Petra van den, Huisman, Marieke, Jansen, Nils, Stoelinga, Mariëlle, van den Bos, Petra, Formal Methods and Tools, and Digital Society Institute

Subjects
22/3 OA procedure
Abstract

Formal analysis techniques for software systems are becoming more and more powerful, and have been used on non-trivial examples. We argue that the next step forward is to combine these different techniques in a single framework, which makes it possible to (i) analyse different parts of the system with different techniques, (ii) apply different techniques on a single component, and (iii) seamlessly combine the results of the various analysis. We describe our vision of how this integration can be achieved for the analysis techniques of testing and deductive verification. We end with an overview of research challenges that need to be addressed to achieve this vision.

Published
2022

48. Reinforcement Learning with Guarantees that Hold for Ever

Author

Hahn, Ernst Moritz, Perez, Mateo, Schewe, Sven, Somenzi, Fabio, Trivedi, Ashutosh, Wojtczak, Dominik, Groote, Jan Friso, Huisman, Marieke, Formal Methods and Tools, and Digital Society Institute

Subjects
2023 OA procedure
Abstract

Reinforcement learning is a successful explore-and-exploit approach, where a controller tries to learn how to navigate an unknown environment. The principle approach is for an intelligent agent to learn how to maximise expected rewards. But what happens if the objective refers to non-terminating systems? We can obviously not wait until an infinite amount of time has passed, assess the success, and update. But what can we do? This talk will tell.

Published
2022

49. Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives

Author

Hahn, Ernst Moritz, Perez, Mateo, Schewe, Sven, Somenzi, Fabio, Trivedi, Ashutosh, Wojtczak, Dominik, Huisman, Marieke, Pasareanu, Corina S., Zhan, Naijun, Formal Methods and Tools, and Digital Society Institute

Subjects
22/1 OA procedure
Abstract

We study the problem of finding optimal strategies in Markov decision processes with lexicographic ω -regular objectives, which are ordered collections of ordinary ω -regular objectives. The goal is to compute strategies that maximise the probability of satisfaction of the first ω -regular objective; subject to that, the strategy should also maximise the probability of satisfaction of the second ω -regular objective; then the third and so forth. For instance, one may want to guarantee critical requirements first, functional ones second and only then focus on the non-functional ones. We show how to harness the classic off-the-shelf model-free reinforcement learning techniques to solve this problem and evaluate their performance on four case studies.

Published
2021

Catalog

Books, media, physical & digital resources
See catalog results