Zobrazeno 1 - 10
of 36
pro vyhledávání: '"Peter Lammich"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 129, Iss Festschrift for Dave Schmidt, Pp 384-403 (2013)
There is a close connection between data-flow analysis and model checking as observed and studied in the nineties by Steffen and Schmidt. This indicates that automata-based analysis techniques developed in the realm of infinite-state model checking c
Externí odkaz:
https://doaj.org/article/1fb0a6a4b1f040ee9653fe7e0d92f5ee
Autor:
Peter Lammich
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms' performance is competitive with their counterparts implemented in C/C++. Our approach is backwards compatible wi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::be49130a95df5db44528fb40bff2b6ff
https://doi.org/10.21203/rs.3.rs-2733052/v1
https://doi.org/10.21203/rs.3.rs-2733052/v1
Publikováno v:
ACM Transactions on Programming Languages and Systems (TOPLAS), 44(3), 14:1-14:36. Association for Computing Machinery (ACM)
Programming Languages and Systems ISBN: 9783030720186
ESOP
Programming Languages and Systems ISBN: 9783030720186
ESOP
We present a framework to verify both, functional correctness and worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structure the reso
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8f3fe9c979db00e943a1e114903d5568
https://research.utwente.nl/en/publications/9f2882bf-66f8-4256-b6a4-67d35f4c63fe
https://research.utwente.nl/en/publications/9f2882bf-66f8-4256-b6a4-67d35f4c63fe
Autor:
Peter Lammich
Publikováno v:
Automated Reasoning ISBN: 9783030510534
IJCAR (2)
IJCAR (2)
Sorting algorithms are an important part of most standard libraries, and both, their correctness and efficiency is crucial for many applications.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::31bc02d8a2addbccac4e953c54f72fbc
https://doi.org/10.1007/978-3-030-51054-1_18
https://doi.org/10.1007/978-3-030-51054-1_18
Publikováno v:
Popescu, A, Lammich, P & Hou, P 2020, ' CoCon: A Conference Management System with Formally Verified Document Confidentiality ', Journal of Automated Reasoning . https://doi.org/10.1007/s10817-020-09566-9
Journal of automated reasoning, 65(2), 321-356. Springer
Journal of automated reasoning, 65(2), 321-356. Springer
We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to speci
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2c31d952606375798c22e32a8f9e324d
http://link.springer.com/10.1007/s10817-020-09566-9
http://link.springer.com/10.1007/s10817-020-09566-9
Autor:
Peter Lammich, Andreas Lochbihler
Publikováno v:
Journal of Automated Reasoning, 63 (1)
We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data structu
Autor:
Peter Lammich
Publikováno v:
Lammich, P 2019, ' Refinement to Imperative HOL ', Journal of Automated Reasoning, vol. 62, no. 4, pp. 481-503 . https://doi.org/10.1007/s10817-017-9437-1
Many algorithms can be implemented most efficiently with imperative data structures. This paper presents Sepref, a stepwise refinement based tool chain for the verification of imperative algorithms in Isabelle/HOL. As a back end we use imperative HOL
Autor:
Peter Lammich, Julian Brunner
Publikováno v:
Brunner, J & Lammich, P 2018, ' Formal Verification of an Executable LTL Model Checker with Partial Order Reduction ', Journal of Automated Reasoning, vol. 60, no. 1, pp. 3-21 . https://doi.org/10.1007/s10817-017-9418-4
We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to
Autor:
Peter Lammich
Publikováno v:
Lammich, P 2019, ' Efficient Verified (UN)SAT Certificate Checking ', Journal of Automated Reasoning . https://doi.org/10.1007/s10817-019-09525-z
SAT solvers decide the satisfiability of Boolean formulas in conjunctivenormal form. They are commonly used for software and hardware verification.Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may invalid
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::77507bba54a50b87dea900ac25666521
https://www.research.manchester.ac.uk/portal/en/publications/efficient-verified-unsat-certificate-checking(7618b7a4-ad98-4bd4-8471-d8ec640e3aaa).html
https://www.research.manchester.ac.uk/portal/en/publications/efficient-verified-unsat-certificate-checking(7618b7a4-ad98-4bd4-8471-d8ec640e3aaa).html
Publikováno v:
EasyChair Preprints.
We verify functional correctness of insertion sort as well as the partition function of quicksort. We use Isabelle/UTP and its denotational semantics for imperative programs as a verification framework. We propose a forward Hoare VCG for our reasonin