Researcher profile

Jürgen Christ

Jürgen Christ contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Logic in Computer Science Programming Languages

Trust snapshot

Quick read

Trust 13 - Baseline

2works

0followers

2topics

2close collaborators

Actions

Decide how to stay connected

Follow researcher0

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2014arXiv

Weakly Equivalent Arrays

The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. Current decision procedures for the theory of arrays saturate the read-over-write and extensionality axioms originally proposed by McCarthy. Various filters are used to limit the number of axiom instantiations while preserving completeness. We present an algorithm that lazily instantiates lemmas based on weak equivalence classes. These lemmas are easier to interpolate as they only contain existing terms. We formally define weak equivalence and show correctness of the resulting decision procedure.

preprint2012arXiv

Towards Bounded Infeasible Code Detection

A first step towards more reliable software is to execute each statement and each control-flow path in a method once. In this paper, we present a formal method to automatically compute test cases for this purpose based on the idea of a bounded infeasible code detection. The method first unwinds all loops in a program finitely often and then encodes all feasible executions of the loop-free programs in a logical formula. Helper variables are introduced such that a theorem prover can reconstruct the control-flow path of a feasible execution from a satisfying valuation of this formula. Based on this formula, we present one algorithm that computes a feasible path cover and one algorithm that computes a feasible statement cover. We show that the algorithms are complete for loop-free programs and that they can be implemented efficiently. We further provide a sound algorithm to compute procedure summaries which makes the method scalable to larger programs.