Zobrazeno 1 - 10
of 45
pro vyhledávání: '"Peter Schachte"'
Precondition inference is a non-trivial problem with important applications in program analysis and verification. We present a novel iterative method for automatically deriving preconditions for the safety and unsafety of programs. Each iteration mai
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5565a6f8f76b96269388615ed657abd8
http://arxiv.org/abs/2108.03178
http://arxiv.org/abs/2108.03178
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783030921231
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::627ea02df21b0e6f7f48bc04decd9868
https://doi.org/10.1007/978-3-030-92124-8_22
https://doi.org/10.1007/978-3-030-92124-8_22
Publikováno v:
Static Analysis ISBN: 9783030888053
SAS
SAS
We revisit disjunctive interval analysis based on the Boxes abstract domain. We propose the use of what we call range decision diagrams (RDDs) to implement Boxes, and we provide algorithms for the necessary RDD operations. RDDs tend to be more compac
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9cffd504797c7972b5c32008fa3c4a11
https://doi.org/10.1007/978-3-030-88806-0_7
https://doi.org/10.1007/978-3-030-88806-0_7
Publikováno v:
Logic-Based Program Synthesis and Transformation ISBN: 9783030684457
LOPSTR
LOPSTR
Given a portfolio of algorithms, the goal of Algorithm Selection (AS) is to select the best algorithm(s) for a new, unseen problem instance. Dynamic Symbolic Execution (DSE) brings together concrete and symbolic execution to maximise the program cove
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c9d977e4e4850f0c1a07bed43cbbc679
http://hdl.handle.net/11585/850377
http://hdl.handle.net/11585/850377
Publikováno v:
Constraints. 24:56-93
Modeling discrete optimization problems is not straightforward. It is often the case that precompiling a subproblem that involves only a few tightly constrained variables as a table constraint can improve solving time. Nevertheless, enumerating all t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b0aae1717a85d428bf9582346f66f768
https://doi.org/10.1007/s10601-018-9297-2
https://doi.org/10.1007/s10601-018-9297-2
Publikováno v:
ARITH
Reasoning about floating-point numbers is notoriously difficult, owing to the lack of convenient algebraic properties such as associativity. This poses a substantial challenge for program analysis and verification tools which rely on precise floating
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::235a4521ffea2597908232c9d80624c7
https://doi.org/10.1109/arith.2019.00038
https://doi.org/10.1109/arith.2019.00038
Publikováno v:
Software: Practice and Experience. 46:1685-1703
Adtpp is an open-source tool that adds support for algebraic data types ADTs to the C programming language. ADTs allow more precise description of program types and more robust handling of data structures than are directly supported by C. ADT definit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3b8107975ac4a9ae619f8d22839c5e88
https://doi.org/10.1002/spe.2407
https://doi.org/10.1002/spe.2407
Publikováno v:
Theoretical Computer Science. 625:1-24
Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on coun
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9e9a59489c3fd13e9e8bfb0909823c0e
https://doi.org/10.1016/j.tcs.2016.01.026
https://doi.org/10.1016/j.tcs.2016.01.026
Autor:
Peter Schachte, Roberto Amadini, Mak Andrlon, Graeme Gange, Peter J. Stuckey, Harald Søndergaard
Publikováno v:
Integration of Constraint Programming, Artificial Intelligence, and Operations Research ISBN: 9783030192112
CPAIOR
CPAIOR
Dynamic Symbolic Execution (DSE) combines concrete and symbolic execution, usually for the purpose of generating good test suites automatically. It relies on constraint solvers to solve path conditions and to generate new inputs to explore. DSE tools
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9cee64d3ced295e6e3c26f31723ba1b4
http://hdl.handle.net/11585/708563
http://hdl.handle.net/11585/708563
Publikováno v:
Programming Languages and Systems ISBN: 9783030341749
APLAS
APLAS
Widening ensures or accelerates convergence of a program analysis, and sometimes contributes a guarantee of soundness that would otherwise be absent. In this paper we propose a generalised view of widening, in which widening operates on values that a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::eb44261abc88b201f081625cad173853
https://doi.org/10.1007/978-3-030-34175-6_6
https://doi.org/10.1007/978-3-030-34175-6_6