Automatic Software Verification: Harnessing Constraint Technologies

Grant number: DP110102579 | Funding period: 2011 - 2015

Completed

Abstract

As we come to rely on software to manage more and more aspects of our lives, the importance of software reliability increases; yet as programs become increasingly complex, reliability becomes ever more elusive. This project will develop automated tools and techniques to ensure that programs do what they were intended to do.

Related publications (9)

Scholarly works icon

Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss

G Gange, JA Navas, P Schachte, H Sondergaard, PJ Stuckey

2015-01-01

The most commonly used integer types have fixed bit-width, making it possible for computations to wrap around, and many programs d..

Scholarly works icon

Truth versus information in logic programming

L Naish, H Sondergaard

2014-11-12

The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-v..

Scholarly works icon

Four-Valued Reasoning and Cyclic Circuits

Graeme Gange, Benjamin Horsfall, Lee Naish, Harald Sondergaard

2014-07-01

Allowing cycles in a logic circuit can be advantageous, for example, by reducing the number of gates required to implement a given..

Scholarly works icon

Failure tabled constraint logic programming by interpolation

G Gange, JA Navas, P Schachte, H Sondergaard, PJ Stuckey

2013-07-01

We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy ..

Scholarly works icon

Abstract Interpretation over Non-Lattice Abstract Domains

G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey

2013-01-01

The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of ..

Scholarly works icon

Solving Difference Constraints over Modular Arithmetic

G Gange, H Sondergaard, PJ Stuckey, P Schachte

2013-01-01

Difference logic is commonly used in program verification and analysis. In the context of fixed-precision integers, as used in ass..

Scholarly works icon

Unbounded model-checking with interpolation for regular language constraints

G Gange, JA Navas, PJ Stuckey, H Sondergaard, P Schachte

2013-01-01

We present a decision procedure for the problem of, given a set of regular expressions R <inf>1</inf>, ..., R <inf>n</inf> , deter..

Scholarly works icon

Logic programming: From underspecification to undefinedness

L Naish, H Søndergaard, B Horsfall

2012-07-24

The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-v..

Scholarly works icon

Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code

JA Navas, P Schachte, H Sondergaard, PJ Stuckey

2012-01-01

Many compilers target common back-ends, thereby avoiding the need to implement the same analyses for many different source languag..