University of Minnesota
Software Engineering Center

You are here

Andrew Gacek

Recent Publications

Towards Synthesis from Assume-Guarantee Contracts involving Infinite Theories: A Preliminary Report

In previous work, we have introduced a contract-based {\em realizability checking} algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arithmetic and uninterpreted functions over infinite domains. This algorithm can determine whether or not it is possible to construct a realization (i.e. an implementation) of an assume-guarantee contract. The algorithm is similar to k-induction model checking, but involves the use of quantifiers to determine implementability.

Reasoning about Algebraic Datatypes with Abstractions

Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain.

Requirements and Architectures for Secure Vehicles

In the High-Assurance Cyber Military Systems project, researchers are investigating how to construct complex networked-vehicle software securely. Experiments demonstrated that careful attention to requirements and system architecture, along with formally verified approaches that remove known security weaknesses, can lead to vehicles that can withstand attacks from even sophisticated attackers with access to vehicle design data.