Author name cluster

Edmund Clarke

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

AIJ Journal 2016 Journal Article

Solving QBF with counterexample guided refinement

Mikoláš Janota
William Klieber
Joao Marques-Silva
Edmund Clarke

This article puts forward the application of Counterexample Guided Abstraction Refinement (CEGAR) in solving the well-known PSPACE-complete problem of quantified Boolean formulas (QBF). The article studies the application of CEGAR in two scenarios. In the first scenario, CEGAR is used to expand quantifiers of the formula and subsequently a satisfiability (SAT) solver is applied. First it is shown how to do that for two levels of quantification and then it is generalized for arbitrary number of levels by recursion. It is also shown that these ideas can be generalized to non-prenex and non-CNF QBF solvers. In the second scenario, CEGAR is employed as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of benchmark families and that the DPLL solver benefits from the additional type of learning.

Details DOI

TCS Journal 2001 Journal Article

The Verus language: representing time efficiently with BDDs

Sérgio Vale Aguiar Campos
Edmund Clarke

There have been significant advances on formal methods to verify complex systems recently. Nevertheless, these methods have not yet been accepted as a realistic alternative to the verification of industrial systems. One reason for this is that formal methods are still difficult to apply efficiently. Another reason is that current verification algorithms are still not efficient enough to handle many complex systems. This work addresses the problem by presenting a language designed especially to simplify writing time-critical programs. It is an imperative language with a syntax similar to C. Special constructs are provided to allow the straightforward expression of timing properties. The familiar syntax makes it easier for non-experts to use the tool. The special constructs make it possible to model the timing characteristics of the system naturally and accurately. A symbolic representation using BDDs, model checking and quantitative algorithms are used to check system timing properties. The efficiency of the representation allows complex realistic systems to be verified.

Details DOI