Tech Talk: Efficient Implementation of Property Directed Reachability

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual date and time for this talk, it is on Monday, 6 February 2012, at 10am.

title: Efficient Implementation of Property Directed Reachability

speaker: Alan Mishchenko

time: Monday, 6 February 2012, 10:00am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Relevant links: the paper, slides for the talk.

bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification.

New tech talk video: Formalizing Haskell 98 in the K semantic framework

We are pleased to announced the availability of a new tech talk video, David Lazar talking about formalizing Haskell 98 in the K semantic framework. For more information, please visit the talk announcement page For more Galois tech talk videos, please visit our Vimeo channel.

Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual time for this talk, it is on Thursday, 12 January 2012

title: On deadlock verification in micro-architectural models of communication fabrics.

speaker: Julien Schmaltz

time: Thursday, 12 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.

bio: Dr. Schmaltz is assistant professor at the Open University of the Netherlands. He is also affiliated with the Digital Security group at the Radboud University Nijmegen. He obtained a PhD from the University of Grenoble in 2006. Before joining the Open University he was a postdoctoral researcher at the University of Saarland (Germany), the Radboud University Nijmegen, and the Embedded System Institute in Eindhoven (The Netherlands). During his PhD, he visited the University of Texas at Austin. His research currently focuses on the use of formal methods in the verification of on-chip communication architectures. His general research interests include the application of formal methods in security, certification, software engineering, hardware design, and model-based testing. He co-authored more than 40 publications. In 2011, he co-chaired the second international conference on Interactive Theorem Proving and the 10th edition of the international workshop on the ACL2 Theorem Prover and its Applications.

Galois Tech Talk (2 of 3 next week!): Model-based Code Generation and Debugging of Concurrent Programs

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual time for this talk, it is on Wednesday, 11 January 2012

title: Model-based Code Generation and Debugging of Concurrent Programs

speaker: Borzoo Bonakdarpour

time: Wednesday, 11 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Design and implementation of distributed systems often involve many subtleties due to their complex structure, non-determinism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from high-level component-based models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multi-party strong synchronization primitives in atomic components by point-to-point send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination.

The second part of the talk will focus on an automated technique for optimal instrumentation of multi-threaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through data-flow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and red-black trees) show significant performance improvement in optimally-instrumented programs using our method as compared to ad-hoc over-instrumented programs.

bio: Borzoo Bonakdarpour is currently a research assistant professor at the School of Computer Science at University of Waterloo, Canada. He was a post-doctoral researcher at the Verimag Laboratory, France, working on the BIP project led by the 2007 Turing Award recipient, Joseph Sifakis. The aim of the project is to develop theory, methods, and tools for building real-time and distributed systems consisting of heterogeneous components. His other research interests include runtime verification, compositional verification of embedded systems, model synthesis and, in particular, automated model repair. He is the main developer of the tool SYCRAFT which is capable of synthesizing fault-tolerant distributed programs of the size 10^80 reachable states and beyond. Borzoo Bonakdarpour obtained his Ph.D. from the Department of Computer Science and Engineering at Michigan State University in 2009. His Ph.D. dissertation, "Automated Revision of Distributed and Real-Time Programs", studies a wide range of model repair problems in closed an open systems and was nominated for the 2010 ACM Doctoral Dissertation Award.

Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Formalizing Haskell 98 in the K Semantic Framework

speaker: David Lazar

time: Tuesday, 10 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Formal semantics is notoriously hard. The K semantic framework is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non-determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K.

The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a work-in-progress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work.

bio: David Lazar is an undergraduate studying computer science at the University of Illinois at Urbana-Champaign. He is one of several developers of the K framework. This summer, he worked on formalizing Haskell in K as a Google Summer of Code student.