Formal Methods Seminar at UIUC

Welcome to the formal methods seminar's website at UIUC. Any UIUC student, visitor or faculty member is welcome to subscribe to our list and to attend our meetings. To subscribe, please follow this link. We currently meet every Friday at 10:00AM in 2124SC, but sometimes there are exceptions, so make sure that you check the exact meeting place, date and time.

Past talks
Past years
Related UIUC Laboratories

Upcoming talks

Friday, September 22nd, 10:00AM, 3405SC

  • Grigore Rosu, University of Illinois at Urbana-Champaign
    Equality of Streams is a $\Pi_2^0$-Complete Problem

    We give a precise characterization for the complexity of the problem of proving equal two streams defined with a finite number of equations: $\Pi_2^0$. Since the $\Pi_2^0$ class includes properly both the recursively enumerable and the co-recursively enumerable classes, this result implies that neither the set of pairs of equal streams nor the set of pairs of unequal streams is recursively enumerable. Consequently, one can find no algorithm for determining equality of streams, as well as no algorithm for determining inequality of streams. In particular, there is no complete proof system for equality of streams and no complete system for inequality of streams.

    This is a post-mortem "preparation" ICFP talk :-)

Past talks

Monday, June 12th, 04:00PM, 2124SC

Friday, May 12th, 10:00AM, 2124SC

  • Matthew Wilding , Rockwell Collins Advanced Technology Center, Cedar Rapids, Iowa
    Formal Verification of a Secure Microprocessor

    Formal models and proofs can help demonstrate that a computer system implementation is correct, and they are required for some kinds of secure system certifications. Rockwell Collins, which has been conducting "formal methods" research for 10+ years, used this approach to establish correct microcode implementation of aspects of its AAMP7G microprocessor. A formal low-level design model of the trusted microcode implementation of the AAMP7G was proved to preserve proper separation that the AAMP7G enforces with its intrinsic partitioning mechanism. The AAMP7G separation correctness theorem proof was developed using the ACL2 theorem prover, and the hundreds of pages of definitions and lemmas that lead ACL2 to accept the separation correctness proof are checked using this publically-available tool. This proof led in part to the National Security Agency's certification of this microprocessor as capable of simultaneously processing information at all levels of classification.

    This work was done in collaboration with David Greve and Raymond Richards of the Rockwell Collins Advanced Technology Center.

    Bio: Matthew Wilding is a principal engineering manager in the Rockwell Collins Advanced Technology Center in Cedar Rapids, Iowa. Dr. Wilding received his PhD in Computer Sciences in 1996 from The University of Texas at Austin, and his research at Rockwell Collins applies formal methods and automated reasoning to critical system development. He currently manages the Advanced Technology Center's Automated Analysis group, which in collaboration with Rockwell Collins product areas and government research sponsors is developing and applying automated analysis to systems with safety and security critical functionality.

Thursday, April 27th, 03:00PM, 2124SC

  • Dr. Byron Cook , Microsoft Research
    Automatically proving the termination of software

    In this talk I will discuss TERMINATOR, which is an automatic program termination prover that supports large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. TERMINATOR is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. The termination argument that TERMINATOR finds is constructed incrementally, based on failed proof attempts. TERMINATOR also infers, and proves, required program invariants on demand. The lecture will close with information about the results of some experiments with TERMINATOR on Windows device drivers.

    Bio: Dr. Byron Cook is researcher at Microsoft's laboratory at Cambridge University. He is also a visiting professor at Chalmers University and at Queen Mary, University of London. Byron interests include automatic formal software verification, automatic theorem proving, and programming language theory. Byron has recently been working on an automatic tool, called TERMINATOR for proving program termination. Byron is also actively investigating methods of proving properties about data structures. Byron developed the SLAM software model checker together with Tom Ball, Vladimir Levin, Jakob Lichtenberg, Sriram Rajamani, and many others. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers.

    Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. Byron's PhD is from OGI.
    For more information about Byron, see http://research.microsoft.com/~bycook .

Friday, February 21st, 10:00AM, 2124SC

  • Darko Marinov , University of Illinois at Urbana-Champaign
    Analyzing the Uses of a Software Modeling Tool

    While a lot of progress has been made in improving analyses and tools that aid software development, little effort has been spent on studying how such tools are commonly used in practice. A study into a tool's usage is important not only because it can help improve the tool's usability but also because it can provide key insights for improving the tool's underlying analysis technology in a common usage scenario. We present a study that explores how (beginner) users work with the Alloy Analyzer, a tool for automatic analysis of software models written in Alloy, a first-order, declarative language. We have modified the analyzer to log (some of) its interactions with the user. Using this modified analyzer, 11 students in two of our graduate classes formulated their Alloy models to solve a problem set. Our analysis of the resulting logs (total of 68 analyzer sessions) shows several interesting observations, and based on them, we propose how to improve the analyzer, both the performance of analyses and the user interaction. Specifically, we show that: (i) users often perform consecutive analyses with slightly different models, and thus incremental analysis can speed up the interaction; (ii) users' interaction with the analyzer are sometimes predictable, and the analyzer can precompute the result of a future action while the user is editing the model; and (iii) (beginner) users can naturally develop semantically equivalent models that have significantly different analysis time.

    Join work with Xiaoming Li, Daryl Shannon, Jabari Walker, and Sarfraz Khurshid.

Friday, April 7th, 3:30PM, 3405SC

  • Cesare Tinelli , University of Iowa
    Formalizing DPLL-based Solvers for Propositional Satisfiability and for Satisfiability Modulo Theories

    The first part of this talk introduces Abstract DPLL, a general rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure, one of the most successful decision procedures for propositional satisfiability. Abstract DPLL allows one to model and formally reason about several DPLL variants and enhancements in a simple way. Its main properties, such as soundness, completeness or termination, immediately carry over to modern DPLL implementations with such advanced features as non-chronological backtracking, lemma learning, and restarts.

    The second part of the talk extends the framework to Satisfiability Modulo Theories (SMT), the problem of determining the satisfiability of quantifier-free formulas in the context of logical theories of interest.

    Abstract DPLL Modulo Theories allows one to formalize a family of SMT techniques that couple a DPLL engine, a generic DPLL-style SAT solver, with a theory solver, a procedure for deciding the satisfiability of sets of literals in a background theory T.

    This is joint work with Robert Nieuwenhuis and Albert Oliveras of the Technical University of Catalonia, and with Clark Barrett of New York University.

    Bio: Dr. Tinelli is an associate professor of Computer Science at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His work concentrates on constraint-based approaches and combination methods for automated reasoning, and their applications to formal verification. His research interests include automated reasoning, formal methods, foundations of programming languages, and applications of logic in computer science. In 2003, Dr. Tinelli received an NSF CAREER award for a project on improving extended static checking of software by means of advanced automated reasoning techniques. He co-leads an international initiative, called SMT-LIB, supported by several research groups in academia and industry, aimed at producing various common standards for SMT-LIB applications as well as a large library theories and benchmarks. Dr. Tinelli has served in the program committee of several conferences and workshops, such as CADE, LPAR, FroCoS, UNIF, PDPAR, and ECAI. He is currently a steering committee member of IJCAR, FTP, and FroCoS, and a trustee of CADE Inc.

Thursday, April 6th, 11:00AM, 2405SC

  • John Rushby , Computer Science Laboratory, SRI International
    SMT Solvers: A Disruptive Technology

    SMT stands for "Satisfiability Modulo Theories": an SMT solver finds satisfying assignments to propositionally complex expressions over combinations of decidable theories such as linear arithmetic and equality with uninterpreted functions.

    The performance of SMT solvers, which are essentially SAT solvers interacting with decision procedures, is increasing rapidly, spurred on by an annual competition. They are a disruptive technology because they have the potential to replace many kinds of special-purpose automation. Beyond the attraction that a single technology can solve many different kinds of problem lies the larger benefit that it may be able to solve mixed problems (e.g., real time plus fault tolerance).

    I will outline the capabilities of SMT solvers and describe their use in formal verification, focusing on verification of real-time systems by infinite bounded model checking. I will also sketch their application to planning in AI, and extensions such as MaxSMT.

    The SAL tool suite, freely available at http://fm.csl.sri.com/, includes the SMT solver ICS and an infinite bounded model checker.
    For an update on SMT solvers, see the competition from CAV 05 http://www.csl.sri.com/users/demoura/smt-comp/index.shtml

Friday, March 17th, 10:00AM, 2124SC

  • Traian Florin Serbanuta , University of Illinois at Urbana-Champaign
    A Semantic Approach to Interpolation

    Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation , we generate, prove and classify more than twenty interpolation results for first-order logic and some for richer logics. A few of these results non-trivially generalize known interpolation results. All the others are new.

    joint work with Andrei Popescu and Grigore Rosu

Friday, March 10th, 10:00AM, 2124SC

  • YoungMin Kwon , University of Illinois at Urbana-Champaign
    Probabilistic modeling and verification of large scale systems

    A notable feature of many proposed Wireless Sensor Networks (WSNs) deployments is their scale: a small system can have more than 50 nodes, sometimes hundreds to thousands of nodes linked together. In such systems, modeling the state of the entire system as a cross-product of the states of individual nodes results in the well-known state explosion problem.

    Instead, we represent the system state by the probability distribution on the state of each node. In other words, the system state represents the probability that a randomly picked node is in a certain state. Although such statistical abstraction of the global state loses some information, it is nevertheless useful in determining many performance metrics of systems that exhibit Markov behavior. We have previously developed a method for specifying the performance metrics of such systems in a probabilistic temporal logic called iLTL and for evaluating the behavior through a novel method for model checking iLTL properties. We extend the iLTL so that it can specify concurrent runs of multiple independent systems. In this paper, we describe a method for estimating the probabilities in a Discrete Time Markov Chain (DTMC) model of a large-scale system. We also provide a statistical test so that we can reject estimated DTMCs if the actual system does not have Markov behavior. We describe results of experiments applying our method to WSNs in an experimental test-bed, as well as using simulations. The results of our experiments suggest that our model estimation and model checking method provides a systematic, precise and easy way of evaluating performance metrics of some large-scale WSNs.

Friday, February 24th, 10:00AM, 2124SC

  • Carlos Pacheco , Massachusetts Institute of Technology (MIT)
    Feedback-directed Random Test Generation

    We present a technique that improves on traditional random testing by incorporating feedback obtained from executing test inputs as they are created. Our technique builds inputs incrementally by randomly selecting a method call to apply and finding arguments from among previously-constructed inputs. As soon as it is built, the input is executed and checked against a set of contracts; the technique then uses the result of the execution to determine if the input is redundant or illegal (if so, the input is discarded), or if it violates a contract (if so, it is made into a test case). Test inputs that exhibit violating behavior are minimized and output as small, failing test cases.

    We have implemented the technique in two tools, RANDOOP (for Microsoft's .Net Framework) and JOE (for Java). To evaluate the technique's effectiveness, we have applied the tools to a set of 14 widely-used libraries comprising 780KLOC, and found many serious errors. Compared with traditional unguided random test generation (as implemented both by us and by an independent tool), feedback-directed test generation finds more bugs, finds more interesting and severe bugs, and produces fewer redundant tests.

    joint wotk with Shuvendu K. Lahiri, Sanjukta Pal, Thomas Ball, and Michael D. Ernst

Friday, February 17th, 10:00AM, 2124SC

  • Zhenmin Li , University of Illinois at Urbana-Champaign
    Applying Data Mining Techniques to Computer Systems

    As computer systems are becoming increasingly complex, it is challenging to provide high performance, reliability and manageability that are demanded by enterprise customers. In order to provide a solution, it is necessary to first analyze and characterize such systems and identify the critical issues. The system data such as source code, running traces, etc. provide a valuable asset for us to target the solution. In the meantime, the huge amount of system data, however, renders a tedious and difficult task on managers and developers, and hence the hidden information would be difficult to extract for system characterization.

    During this talk, I will present a novel approach to analyze various system data by applying data mining techniques. This approach can effectively obtain useful information hidden in huge amount of system data and then we can exploit such information to improve system performance, reliability and manageability. Specifically, we apply different data mining algorithms on different types of system data such as source code, access traces, and system call traces, to achieve different goals including automated debugging and system behavior characterization. The results demonstrate that using data mining techniques is an efficient and effective approach to solving computer system problems.

    Bio: Zhenmin Li is a PhD student supervised by Prof. Yuanyuan Zhou. His research interests include computer systems, software reliability, data mining, storage systems, and energy management. He received his BE and ME in computer science from Tsinghua University, China. Further information is available at http://opera.cs.uiuc.edu/~zli4

Friday, February 10th, 10:00AM, 2124SC

  • Elsa Gunter , University of Illinois at Urbana-Champaign
    Types for Security in a Mobile World

    Our society is increasingly moving towards richer forms of information exchange where mobility of processes and devices plays a prominent role. This tendency has prompted the academic community to study the security problems arising from such mobile environments, and in particular, the security policies regulating who can access the information in question.

    In this talk we propose a calculs for mobile agents and a type system for specifying access privileges based on a combination of the identity of the user seeking access, its credentials, and the location from which he seeks it, within a reconfigurable nested structure.

    We define BACI_R, a boxed ambient calculus extended with a Distributed Role-Based Access Control mechanism where each ambient controls its own access policy. A process in BACI_R is associated with an owner and a set of activated roles that grant permissions for mobility and communication. The calculus includes primitives to activate and deactivate roles. The behavior of these primitives is determined by the process?s owner, its current location and its currently activated roles. We consider two forms of security violations that our type system prevents: 1) attempting to move into an ambient without having the authorizing roles granting entry activated and 2) trying to use a communication port without having the roles required for access activated. We accomplish 1) and 2) by giving a static type system, an untyped transition semantics, and a typed transition semantics. We then show that a well-typed program never violates the dynamic security checks.

Friday, February 3rd, 10:00AM, 2124SC

  • Koushik Sen, University of Illinois at Urbana-Champaign
    Scalable Automated Methods for Software Reliability

    Testing with manually generated test cases is the primary technique used in industry to improve reliability of software--in fact, such testing is reported to account for over half of the typical cost of software development. I will describe Concolic Testing, an efficient approach which combines random and symbolic testing. Concolic testing enables automatic and systematic testing of large programs, avoids redundant test cases and does not generate false warnings. Experiments on real-world software show that concolic testing can be used to effectively catch generic errors such as assertion violations, memory leaks, uncaught exceptions, and segmentation faults. Combined with dynamic partial order reduction techniques, concolic testing is effective in catching concurrency bugs such as data races and deadlocks. I will describe my experience with building two concolic testing tools, CUTE for C programs and jCUTE for Java programs, and applying these tools to real-world software systems. Finally, I will provide a brief overview of my research in predictive runtime monitoring, statistical and probabilistic model checking, application of machine learning to verify infinite state systems, and probabilistic programming.

Past years

2005

Monday, December 5th, 10:00AM, 2124SC

  • Mahesh Viswanathan, University of Illinois at Urbana-Champaign
    A Higher Order Modal Fixpoint Logic

    We present a higher order modal fixed point logic (HFL) that extends the modal $\mu$-calculus to allow predicates on states (sets of states) to be specified using recursively defined higher order functions on predicates. The logic HFL includes negation as a first-class construct and uses a simple type system to identify the monotonic functions on which the application of fixed point operators is semantically meaningful. The model checking problem for HFL over finite transition systems remains decidable, but its expressiveness is rich. We construct a property of finite transition systems that is not expressible in the Fixed Point Logic with Chop (FLC) but which can be expressed in HFL. A similar argument is used to show that HFL is strictly more expressive, even over finite transition systems, than the restriction of HFL to any fixed order. Over infinite transition systems, we show that HFL can express bisimulation and simulation of push down automata, and any recursively enumerable property of a class of transition systems representing the natural numbers.

Monday, November 28th, 10:00AM, 2124SC

  • Koushik Sen, University of Illinois at Urbana-Champaign
    An Automated Scalable Approach for Improving Software Quality

    Software testing accounts for an estimated 50% of the total cost of software development. We present an automated scalable approach to improve software reliability and security of real-world software systems. The approach combines a number of novel techniques, which include a combination of random and symbolic testing, runtime partial order reduction, predictive analysis, and runtime monitoring. Based on this approach, we have developed tools and combined them to provide a complete automated testing and runtime monitoring solution for software. The results of applying this tool and its components to real-world software were encouraging. For example, CUTE, a tool implementing concolic testing, found two previously unknown errors -- a segmentation fault and an infinite loop -- in SGLIB, a popular C data-structure library used in a commercial software. On the other hand, DART has been successfully used at Bell-laboratories, Lucent Technologies, to test and debug open-source session initiation protocol and other real-world protocol implementations. The extension of CUTE to concurrent Java programs, called jCUTE, found a subtle time-partitioning error in the Honeywell's DEOS real-time operating system developed for use in small business aircraft. The runtime monitoring engine \textsc{Eagle}, which is used in conjunction with testing, has been used successfully to analyze NASA's K9 Mars Rover and to \emph{identify security attacks in DARPA logs}. Finding these bugs took a few seconds to a minute. In contrast, many other tools either missed those errors or found those bugs after hours of search.

Monday, November 14th, 10:00AM, 2124SC

  • Madhusudan Parthasarathy, University of Illinois at Urbana-Champaign
    Making the stack visible: visibly pushdown languages

    We study visibly pushdown languages, a subclass of context-free languages defined using pushdown automata where the input determines the stack operations permitted. Most usages of context-free languages seem to only require this subclass, and surprisingly, it turns out that this subclass is very well behaved: it is closed under all boolean operations, inclusion and equivalence are decidable, etc. In the verification context, it provides a theory for how to check programs with recursion against correctness properties that require the stack. We will also show robustness of this class by giving logical and tree-automata characterizations, and will also briefly look at its extension to infinite words.

    Visibly pushdown languages hence emerge as a tractable insertion into the Chomsky hierarchy worthy of study (and perhaps a class that can be introduced in a basic theory-of-computation course).

  • Viraj Kumar, University of Illinois at Urbana-Champaign
    Congruences for visibly pushdown languages

    We study congruences on words in order to characterize the class of visibly pushdown languages (VPL). For any language L, we define a natural congruence on words that resembles the syntactic congruence for regular languages, such that this congruence is of finite index if, and only if, L is a VPL. We then study the problem of finding canonical minimal deterministic automata for VPL. Though {\VPL}s in general do not have unique minimal automata, we consider a subclass of VPAs called k-module single-entry VPAs that correspond to programs with recursive procedures without input parameters, and show that the class of well-matched VPLs do indeed have unique minimal k-module single-entry automata. We also give a polynomial time algorithm that minimizes such k-module single-entry VPAs.

Monday, October 31, 10:00AM, 2124SC

  • Moshe Y. Vardi, Rice University
    The Design of A Formal Property-Specification Language

    In recent years, the need for formal specification languages is growing rapidly as the functional validation environment in semiconductor design is changing to include more and more validation engines based on formal verification technologies. In particular, the usage of Formal Equivalence Verification and Formal Property Verification is growing, new symbolic simulation engines are introduced and hybrid environments of scalar and symbolic simulators are developed. To facilitate the use of these new-generation validation engines - properties, checkers and reference models need to be developed in a formal language.

    In this talk we describe the design of the ForSpec Temporal Logic (FTL), the temporal logic of ForSpec, Intel's new formal property-specification language, which is today part of Synopsis OpenVera hardware verification language (www.open-vera.com). The key features of FTL are: it is a linear temporal logic, based on Pnueli's LTL, it enables the user to define temporal connectives over time windows, it enables the user to define regular events, which are regular sequences of Boolean events, and then relate such events via special connectives, and it contains constructs that enable the user to model multiple clock and reset signals, which is useful in the verification of globally asynchronous and locally synchronous hardware designs.

    The focus of the talk is on design rationale, rather than a detailed language description.

Monday, October 24th, 10:00AM, 2124SC

  • Grigore Rosu, University of Illinois at Urbana-Champaign
    Continuation-based Rewriting Logic Definitions of Programming Languages

    A technique to define programming languages in rewriting logic is presented. Based on a first-order representation of continuations and on matching modulo associativity, commutativity and identity, the technique is introduced by defining a non-trivial concurrent higher-order programming language. The rewrite logic definition of a language can serve multiple purposes: (1) it can be executed on rewrite engines, thus providing potentially very efficient interpreters; (2) it can be formally analyzed with analysis tools, such as model checkers, for rewrite logic theories; (3) it gives an initial model semantics, amenable to inductive theorem proving. Moreover, the presented definitional technique is easy to understand and teach, compact, modular and scales well.

Monday, October 17th, 10:00AM, 3405SC

  • Yuri Gurevich, Microsoft Research
    Interactive Algorithms

    We report on the study of interactive algorithms within the framework of behavioral computation theory. First we describe what behavioral computation theory is, and then we consider a single sequential-time algorithm interacting intra-step with the rest of the world.

    Such interaction is more common that one may think: input and output operations, remote procedure calls, receiving and sending mail, making non-deterministic choices, creating new objects, ping commands, print commands, and so on. Does nondeterminism really involve interaction? It does; all by itself, an algorithm is inherently deterministic. Similarly, the NEW command is nothing but a cry for help.

    There are numerous communication mechanisms: remote procedure calls, messages, single-answer queries, multiple-answer queries, and so on. Is there a simple universal communication mechanism? Yes, and we will exhibit such a mechanism.

    Finally, we will present interactive abstract state machine and a characterization theorem: every interactive algorithm is behaviorally equivalent to an interactive abstract state machine.

    This is joint work with Andreas Blass, Benjamin Rossman and Dean Rosenzweig. A more extended abstract is found in article #175 at the speaker's website. Many (but not all) details are found in articles #166, #170, #171, #176 at the website.

    Bio:
    Yuri Gurevich is Sr. Researcher at Microsoft Research in Redmond, WA. He is also Professor Emeritus at the University of Michigan, ACM Fellow, Guggenheim Fellow, and Dr. Honoris Causa of Limburg University in Belgium.

Monday, October 10th, 10:00AM, 2124SC

  • Ralf Sasse, University of Illinois at Urbana-Champaign
    Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics

    This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic calculus which is implemented in the interactive prover of the KeY system. As a basis for validation, we take an existing SOS style rewriting logic semantics for Java, formalized in the input language of the Maude system. That semantics is lifted to cope with schematic programs like the ones appearing in program transformation rules. The rewriting theory is further extended to generate valid initial states for involved program fragments, and to check the final states for equivalence. The result is used in nightly validation runs over the relevant fragment of the calculus in the KeY system.

Monday, October 3rd, 10:00AM, 2405SC

  • Dana S. Scott, Carnegie Mellon University (Retired)
    TOPOLOGY, CATEGORIES, and LAMBDA-CALCULUS

    Many categories have injective objects, but their properties depend on what families of subobjects are allowed. In the case of topological T_0-spaces, for example, two alternatives suggest themselves: (1) arbitrary subspaces, and (2) dense subspaces. Both notions are interesting. Thus, a space D is injective in sense (1) iff for any space Y and subspace X and any continuous function f:X->D there is a continuous extension f':Y->D of f. Injective spaces are easily proved to be closed under arbitrary products and continuous retracts, which facts provide many examples once a few such spaces are known. Perhaps it is not so obvious, however, that injective spaces are also closed under the formation of function spaces, once the space of continuous functions is given the right topology; indeed the category of injective spaces and continuous functions is a cartesian closed category. The talk will review old and new results about injective spaces, applications of the results, and a recent use of injectives to define a cartesian closed extension of the category of all T_0-spaces. This topological point of view makes it obvious that (untyped) lambda-calculus models exist in many forms. A suitable choice of an injective space also shows how a notion of computability transfers to many familiar spaces.

Monday, September 26th, 10:00AM, 2124SC

  • Timo Latvala, University of Illinois at Urbana-Champaign
    Incremental and Complete Bounded Model Checking for Full PLTL

    joint work with Keijo Heljanko, Tommi Junttila, Helsinki University of Technology and Armin Biere, ETH Zurich

    Bounded model checking is an efficient method for finding bugs in system designs. The major drawback of the basic method is that it cannot prove properties, only disprove them. Recently, some progress has been made towards proving properties of LTL using bounded model checking. We present an incremental and complete bounded model checking method for the full linear temporal logic with past (PLTL). Compared to previous works, our method both improves and extends current results in many ways:

    (i) Our encoding is incremental, maximizing the potential gain of using incremental SAT-solvers. (ii) We can prove non-existence of a counterexample at shallower depths than previous techniques in many cases. (iii) We support full PLTL.

    We have implemented our method in the NuSMV2 model checker and report encouraging experimental results.

  • Sumant Kowshik, University of Illinois at Urbana-Champaign
    Statically guaranteeing critical system behaviour in the presence of untrusted components in real-time control

    The increasing demand for functionality and performance in real-time control systems have led to the interaction between trusted and untrusted components in the system. In this work, we statically analyze the trusted and untrusted components in the system to determine if critical functionality is dependent on errors in untrusted components in the system.

Monday, September 19th, 10:00AM, 2124SC

  • Jose Meseguer, University of Illinois at Urbana-Champaign
    A categorical Approach to Simulations

    joint work with Miguel Palomino and Narciso Marti-Oliet

    Simulations between Kripke Structures are a very useful way to relate concurrent systems for verification purposes. They are useful because they allow us to relate different levels of abstraction of a system, and also because they reflect logical properies (in the backward direction).

    Simulations compose, thus forming a category; however, the categorical properties of simulations do not seem to have been studied much previously. In this talk, the notion of simulation is generalized as much as possible, leading to several (increasingly more general) categories. The relation of such categories to temporal logic, in the sense of being categories of models for temporal logic institutions, and also in the sense of reflection of properties is also discussed.

Monday, September 12th, 10:00AM, 2124SC

  • Darko Marinov, University of Illinois at Urbana-Champaign
    Symstra: A Framework for Generating Object-Oriented Unit Tests using Symbolic Execution

    joint work with Tao Xie, Wolfram Schulte, and David Notkin.

    Object-oriented unit tests consist of sequences of method invocations. Behavior of an invocation depends on the method's arguments and the state of the receiver at the beginning of the invocation. Correspondingly, generating unit tests involves two tasks: generating method sequences that build relevant receiverobject states and generating relevant method arguments. This paper proposes Symstra, a framework that achieves both test generation tasks using symbolic execution of method sequences with symbolic arguments. The paper defines symbolic states of object-oriented programs and novel comparisons of states. Given a set of methods from the class under test and a bound on the length of sequences, Symstra systematically explores the object-state space of the class and prunes this exploration based on the state comparisons. Experimental results show that Symstra generates unit tests that achieve higher branch coverage faster than the existing test-generation techniques based on concrete method arguments.

  • Marcelo d'Amorim, University of Illinois at Urbana-Champaign
    Eclat: Automatic Generation and Classification of Test Inputs

    Article by: Carlos Pacheco and Michael D. Ernst

    This paper describes a technique that selects, from a large set of test inputs, a small subset likely to reveal faults in the software under test. The technique takes a program or software component, plus a set of correct executions---say, from observations of the software running properly, or from an existing test suite that a user wishes to enhance. The technique first infers an operational model of the software's operation. Then, inputs whose operational pattern of execution differs from the model in specific ways are suggestive of faults. These inputs are further reduced by selecting only one input per operational pattern. The result is a small portion of the original inputs, deemed by the technique as most likely to reveal faults. Thus, the technique can also be seen as an error-detection technique.

    The paper describes two additional techniques that complement test input selection. One is a technique for automatically producing an oracle (a set of assertions) for a test input from the operational model, thus transforming the test input into a test case. The other is a classification-guided test input generation technique that also makes use of operational models and patterns. When generating inputs, it filters out code sequences that are unlikely to contribute to legal inputs, improving the efficiency of its search for fault-revealing inputs.

    We have implemented these techniques in the Eclat tool, which generates unit tests for Java classes. Eclat's input is a set of classes to test and an example program execution---say, a passing test suite. Eclat's output is a set of JUnit test cases, each containing a potentially fault-revealing input and a set of assertions at least one of which fails. In our experiments, Eclat successfully generated inputs that exposed fault-revealing behavior; we have used Eclat to reveal real errors in programs. The inputs it selects as fault-revealing are an order of magnitude as likely to reveal a fault as all generated inputs.

Related UIUC Labs
Last update: Wednesday, September 20th, 2006
tserban2@uiuc.edu