Related papers: Automated Termination Proofs for C Programs with L…
Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same…
GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with…
Slicing is a program analysis technique originally developed for imperative languages. It facilitates understanding of data flow and debugging. This paper discusses slicing of Constraint Logic Programs. Constraint Logic Programming (CLP) is…
Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a…
2LS ("tools") is a verification tool for C programs, built upon the CPROVER framework. It allows one to verify user-specified assertions, memory safety properties (e.g. buffer overflows), numerical overflows, division by zero, memory leaks,…
Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of…
The advantages of tabled evaluation regarding program termination and reduction of complexity are well known --as are the significant implementation, portability, and maintenance efforts that some proposals (especially those based on…
In this preliminary note, we will illustrate our ideas on automated mechanisms for termination and non-termination reasoning.
We show how definite extended logic programs can be used for defining and reasoning with rough sets. Moreover, a rough-set-specific query language is presented and an answering algorithm is outlined. Thus, we not only show a possible…
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…
These notes outline a formal method for program verification of numerical computation. It forms the basis of the software package VPC in its initial phase of development. Much of the style of presentation is in the form of notes that…
Given a program and a time deadline, does the program finish before the deadline when executed on a given platform? With the requirement to produce a test case when such a violation can occur, we refer to this problem as the worst-case…
Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. We propose a sound transformation of the program to verify, enabling SC tools to…
Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly…
We empirically evaluate the finite-time performance of several simulation-optimization algorithms on a testbed of problems with the goal of motivating further development of algorithms with strong finite-time performance. We investigate if…
Computational reductions are an important and powerful concept in computer science. However, they are difficult for many students to grasp. In this paper, we outline a concept for how the learning of reductions can be supported by…
The termination problem for affine programs over the integers was left open in\cite{Braverman}. For more that a decade, it has been considered and cited as a challenging open problem. To the best of our knowledge, we present here the most…
We apply proof-theoretic techniques in answer Set Programming. The main results include: 1. A characterization of continuity properties of Gelfond-Lifschitz operator for logic program. 2. A propositional characterization of stable models of…
Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite the use of Satisfiability Modulo Theories (SMT) solvers to…
Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is mainly…