Zobrazeno 1 - 10
of 371
pro vyhledávání: '"Rümmer, P."'
Autor:
Wolff, Sebastian, Gupta, Ekanshdeep, Esen, Zafer, Hojjat, Hossein, Rümmer, Philipp, Wies, Thomas
Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils down to analyzing the possible shapes of data structures, leading to t
Externí odkaz:
http://arxiv.org/abs/2408.09037
Publikováno v:
EPTCS 402, 2024, pp. 118-130
The input language for today's CHC solvers are commonly the standard SMT-LIB format, borrowed from SMT solvers, and the Prolog format that stems from Constraint-Logic Programming (CLP). This paper presents a new front-end of the Eldarica CHC solver t
Externí odkaz:
http://arxiv.org/abs/2404.14924
Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequences are natural abstractions of extendable arrays, which permit a we
Externí odkaz:
http://arxiv.org/abs/2308.00175
In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to tra
Externí odkaz:
http://arxiv.org/abs/2306.00004
We present RETA (Relative Timing Analysis), a differential timing analysis technique to verify the impact of an update on the execution time of embedded software. Timing analysis is computationally expensive and labor intensive. Software updates rend
Externí odkaz:
http://arxiv.org/abs/2304.14213
Autor:
Hojjat, Hossein, Rümmer, Philipp
Publikováno v:
EPTCS 373, 2022, pp. 35-43
This paper describes an ongoing effort to develop an optimizing version of the Eldarica Horn solver. The work starts from the observation that many kinds of optimization problems, and in particular the MaxSAT/SMT problem, can be seen as search proble
Externí odkaz:
http://arxiv.org/abs/2211.12229
Learning program semantics from raw source code is challenging due to the complexity of real-world programming language syntax and due to the difficulty of reconstructing long-distance relational information implicitly represented in programs using i
Externí odkaz:
http://arxiv.org/abs/2206.06986
Theories over strings are among the most heavily researched logical theories in the SMT community in the past decade, owing to the error-prone nature of string manipulations, which often leads to security vulnerabilities (e.g. cross-site scripting an
Externí odkaz:
http://arxiv.org/abs/2112.06039
Autor:
Chen, Taolue, Lamas, Alejandro Flores, Hague, Matthew, Han, Zhilei, Hu, Denghang, Kan, Shuanglong, Lin, Anthony Widjaja, Ruemmer, Philipp, Wu, Zhilin
Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features
Externí odkaz:
http://arxiv.org/abs/2111.04298
Autor:
Fedyukovich, Grigory, Rümmer, Philipp
Publikováno v:
EPTCS 344, 2021, pp. 91-108
CHC-COMP-21 is the fourth competition of solvers for Constrained Horn Clauses. In this year, 7 solvers participated at the competition, and were evaluated in 7 separate tracks on problems in linear integer arithmetic, linear real arithmetic, arrays,
Externí odkaz:
http://arxiv.org/abs/2109.04635