Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Lukas Bulwahn"'
Publikováno v:
CCSW@CCS
Proceedings of the 2020 ACM SIGSAC Conference on Cloud Computing Security Workshop
Proceedings of the 2020 ACM SIGSAC Conference on Cloud Computing Security Workshop
Public development processes are a key characteristic of open source projects. However, fixes for vulnerabilities are usually discussed privately among a small group of trusted maintainers, and integrated without prior public involvement. This is sup
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::797848a47701fe4ae2c21fe432b7f1d6
https://doi.org/10.1145/3411495.3421360
https://doi.org/10.1145/3411495.3421360
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 257
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ef468139f12f2c15a264bea6d11b1d5e
https://doi.org/10.4204/eptcs.257.0
https://doi.org/10.4204/eptcs.257.0
Publikováno v:
Automated Driving ISBN: 9783319318936
This paper discusses the need and requirements for an open dependable power-computing (DPC) platform (including operating system, middleware, update process, etc.) to support advanced assisted and automated driving functions. Automated driving functi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::02147971a3f96c37b3ac2eb8ac8b95a9
https://doi.org/10.1007/978-3-319-31895-0_14
https://doi.org/10.1007/978-3-319-31895-0_14
Autor:
Lukas Bulwahn
Publikováno v:
Logic for Programming, Artificial Intelligence, and Reasoning ISBN: 9783642287169
LPAR
LPAR
We present a novel counterexample generator for the interactive theorem prover Isabelle based on a compiler that synthesizes test data generators for functional programming languages (e.g. ML, Haskell) from specifications in Isabelle. In contrast to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a81f37fd9f03a8ba8ce3017a826d01a0
https://doi.org/10.1007/978-3-642-28717-6_14
https://doi.org/10.1007/978-3-642-28717-6_14
Autor:
Lukas Bulwahn
Publikováno v:
Certified Programs and Proofs ISBN: 9783642353079
CPP
CPP
The new Quickcheck is a counterexample generator for Isabelle/HOL that uncovers faulty specifications and invalid conjectures using various testing strategies. The previous Quickcheck only tested conjectures by random testing. The new Quickcheck exte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::79fd91409ce423c4c3dfacc1fe4a6686
https://doi.org/10.1007/978-3-642-35308-6_10
https://doi.org/10.1007/978-3-642-35308-6_10
Publikováno v:
Frontiers of Combining Systems ISBN: 9783642243639
FroCoS
FroCoS
Isabelle/HOL is a popular interactive theorem prover based on higherorder logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on resolution p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cd2a02923ee6e8b79a6c4becc303e696
https://doi.org/10.1007/978-3-642-24364-6_2
https://doi.org/10.1007/978-3-642-24364-6_2
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642033582
TPHOLs
TPHOLs
Inductively defined predicates are frequently used in formal specifications. Using the theorem prover Isabelle , we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis;
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d0e74f64c50656f53bd2e4b0e6e9e830
https://doi.org/10.1007/978-3-642-03359-9_11
https://doi.org/10.1007/978-3-642-03359-9_11
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540710653
TPHOLs
TPHOLs
We introduce a lightweight approach for reasoning about programs involving imperative data structures using the proof assistant Isabelle/HOL. It is based on shallow embedding of programs, a polymorphic heap model using enumeration encodings and type
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5529aa722111a56f183790c4d0ec5d07
https://doi.org/10.1007/978-3-540-71067-7_14
https://doi.org/10.1007/978-3-540-71067-7_14
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540745907
TPHOLs
TPHOLs
We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4b7537903326308ae47ed1a7ba834357
https://doi.org/10.1007/978-3-540-74591-4_5
https://doi.org/10.1007/978-3-540-74591-4_5
Publikováno v:
EPTCS
FVAV 2017-1st Formal Verification of Autonomous Vehicles Workshop
FVAV 2017-1st Formal Verification of Autonomous Vehicles Workshop, Sep 2017, Turin, Italy. pp.91--104, ⟨10.4204/EPTCS.257.9⟩
Electronic Proceedings in Theoretical Computer Science, Vol 257, Iss Proc. FVAV 2017, Pp 91-104 (2017)
FVAV@iFM
FVAV 2017-1st Formal Verification of Autonomous Vehicles Workshop
FVAV 2017-1st Formal Verification of Autonomous Vehicles Workshop, Sep 2017, Turin, Italy. pp.91--104, ⟨10.4204/EPTCS.257.9⟩
Electronic Proceedings in Theoretical Computer Science, Vol 257, Iss Proc. FVAV 2017, Pp 91-104 (2017)
FVAV@iFM
We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further inst
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bd479820cc006e65f633e5757d159556
https://hal.science/hal-01657848
https://hal.science/hal-01657848