Zobrazeno 1 - 10
of 34
pro vyhledávání: '"Daniel Dietsch"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 296, Iss Proc. HCVS/PERR 2019, Pp 42-47 (2019)
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attractive properties in terms of expressiveness and accessibility to algorith
Externí odkaz:
https://doaj.org/article/84307c3c848847f48d9e2d368e631a4c
Autor:
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, Michael Tautschnig
Publikováno v:
ACM Transactions on Software Engineering and Methodology. 31:1-69
Over the last years, witness-based validation of verification results has become an established practice in software verification: An independent validator re-establishes verification results of a software verifier using verification witnesses, which
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b4ee099f4f8e595b0c1d6ee1d39c3d2b
https://doi.org/10.1145/3477579
https://doi.org/10.1145/3477579
Autor:
Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, Andreas Podelski
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308192
The verification approach of Ultimate Automizer utilizes SMT formulas. This paper presents techniques to keep the size of the formulas small. We focus especially on a normal form, called CommuHash normal form that was easy to implement and had a sign
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b8a7a8c9a93f1f36bbb8faea8ff11ff5
https://doi.org/10.1007/978-3-031-30820-8_39
https://doi.org/10.1007/978-3-031-30820-8_39
Autor:
Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995263
Ultimate GemCutterverifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleav
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c7cabbd3f2bde6940f46e0be99748d0f
https://doi.org/10.1007/978-3-030-99527-0_35
https://doi.org/10.1007/978-3-030-99527-0_35
Autor:
Daniel Dietsch, Vincent Langenfeld
Publikováno v:
Proceedings of the Annual Hawaii International Conference on System Sciences.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::90b85074722bcb12290868d3cbe2eb38
https://doi.org/10.24251/hicss.2022.119
https://doi.org/10.24251/hicss.2022.119
Autor:
Eric Koskinen, Daniel Dietsch, Georgios Portokalidis, Ton Chanh Le, Chengbin Pang, Jun Xu, Yuandong Cyrus Liu
Publikováno v:
Programming Languages and Systems ISBN: 9783030890506
There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3211f78a86a3d0e0fb2afceb4a8e83f5
https://doi.org/10.1007/978-3-030-89051-3_16
https://doi.org/10.1007/978-3-030-89051-3_16
Autor:
Mehdi Naouar, Matthias Heizmann, Daniel Dietsch, Andreas Podelski, Claus Schätzle, Dominik Klumpp
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030670665
VMCAI
VMCAI
Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be solv
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9f25def55be3513e2b44c17a67cd66c9
https://doi.org/10.1007/978-3-030-67067-2_9
https://doi.org/10.1007/978-3-030-67067-2_9
Publikováno v:
Networked Systems ISBN: 9783030910136
Networked Systems
Networked Systems
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b1c08e1e469044a3ddeae47141d5f2dc
https://doi.org/10.1007/978-3-030-91014-3_12
https://doi.org/10.1007/978-3-030-91014-3_12
Publikováno v:
2020 IEEE Workshop on Formal Requirements (FORMREQ).
With today’s increasing complexity of systems andrequirements there is a need for formal analysis of requirements.Although there exist several formal requirements description lan-guages and corresponding analysis tools that target an industrialaudi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4051634409e6f16cd9a50e383ebaea67
https://doi.org/10.1109/formreq51202.2020.00010
https://doi.org/10.1109/formreq51202.2020.00010
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030452360
TACAS (2)
TACAS (2)
Ultimate Taipan is a software model checker that combines trace abstraction with abstract interpretation on path programs. In this year’s version, we replaced our abstract interpretation engine and now use a combination of multiple abstraction func
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c61b525e5fc4f53a528f7a8d57956d3d
https://doi.org/10.1007/978-3-030-45237-7_32
https://doi.org/10.1007/978-3-030-45237-7_32