Viewing 1 current event matching “formal methods” by Date.
Sort By: Date  Event Name, Location , Default 

Friday
Aug 24

Galois Tech Talk: Reasoning about Critical Systems using Refinement – Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building) Abstract: Verification is often the dominant cost in the design of critical systems. In this talk, we advocate the use of refinement to reason about critical systems. The idea is that a system is correct if all of its observable behaviors are allowed by an abstract system that acts as the specification. For example, to verify a microprocessor using refinement, one shows that it implements its instruction set architecture. We provide a general introduction to refinement and motivate the need for various notions of refinement. We present various techniques and methods that have been developed to facilitate mechanized reasoning. We discuss the use of refinement for reasoning about distributed systems and hardware. Bio: Pete Manolios is a Professor in the College of Computer and Information Science at Northeastern. Pete’s primary research interest is mechanized formal verification and validation of computational systems. Pete has served as an Associate Editor of ACM Transactions on Design Automation of Electronic Systems (TODAES), as a member of the FMCAD, ACL2 and ITP Steering Committees, and is a member of the IFIP working group 1.9/2.15 on Verified Software. 
Viewing 24 past events matching “formal methods” by Date.
Sort By: Date  Event Name, Location , Default 

Monday
Nov 17, 2008

FMCAD 2008 (Formal Methods in Computer Aided Design) through Embassy Suites PortlandDowntown Important DatesEarly Registration Deadline: October 14, 2008 Hotel Registration Deadline: October 18, 2008 Conference OverviewFMCAD 2008 is the eighth in a series of conferences on the theory and application of formal methods in hardware and system design and verification. In 2005, the biannual FMCAD and sister conference CHARME decided to merge to form an annual conference with a unified community. The resulting unified FMCAD provides a leading international forum to researchers and practitioners in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for formally reasoning about computing systems, as well as open challenges therein. Local InformationThe Conference will be held at the Embassy Suites (Downtown) in Portland, Oregon. We have negotiated a special rate with the hotel for conference attendees. Please book early to secure the reduced rate. For details, please see the conference web page. A dinner cruise on the Willamette River is planned. Technical ProgramThe technical program is available at the conference web page. It includes 2 invited keynotes, 4 invited tutorials, 24 regular papers, 4 short papers, and 2 panels. Keynotes o Ken McMillan (Cadence): Interpolation  Theory and Applications o Carl Seger (Intel): Formal Methods and Physical Design: Match Made in Heaven or Fools' Paradise? Tutorials o Kevin Jones (Rambus): Analog and Mixed Signal Verification: The State of the Art and some Open Problems o Moshe Levinger (IBM): Building a Bridge: From PreSilicon Verification to PostSilicon Validation o Byron Cook (Microsoft): Computing Bounds on Space and Time for Hardware Compilation. o David Hardin (Rockwell Collins): Considerations in the Design and Verification of Microprocessors for SafetyCritical and SecurityCritical Applications. Panels o High Level Design and ESL: Who Cares? o The Future of Formal: Academic, IC, EDA, and Software Perspectives Sponsors
In cooperation with: ACM SIGDA Financial support: Cadence, Galois, IBM, Intel, NEC, Synopsys 
Tuesday
Oct 27, 2009

Galois Talk: How to choose between a screwdriver and a drill – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/20/crenshawsimplex/ An RSVP is not required; but feel free to drop a line to [email protected]om if you've any questions or comments. Levent Erkok 
Tuesday
Feb 2, 2010

Galois Tech Talk: "An Introduction to the Maude Formal Tool Environment" – Galois, Inc Hello, The next Galois Tech Talk will be "An Introduction to the Maude Formal Tool Environment", presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am. For more details, please visit: http://www.galois.com/blog/2010/01/29/techtalkanintroductiontothemaudeformaltoolenvironment/ Hope to see you there! Iavor 
Monday
May 24, 2010

Galois Tech Talk: The L4.verified Project – Galois, Inc The L4.verified Project Presented by Dr. Gerwin Klein. Last year, the NICTA L4.verifed project produced a formal machinechecked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security. 
Tuesday
Jun 15, 2010

Galois Tech Talk: Introducing WellFounded Recursion – Galois, Inc Introducing WellFounded Recursion Eric Mertens Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of wellfounded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort. 
Tuesday
Nov 9, 2010

Galois Tech Talk: Copilot: A Hard RealTime Runtime Monitor – Galois, Inc Presented by Lee Pike. We address the problem of runtime monitoring for hard realtime programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a streambased dataflow language that generates small constanttime and constantspace C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying realtime operating system. This talk will include fun pictures and videos. 
Tuesday
Nov 16, 2010

Galois Tech talk: Formal Methods Applied to Control Software – Galois, Inc speaker: Alwyn Goodloe Critical cyberphysical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the FramaC tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers. 
Tuesday
Jan 25, 2011

Galois tech talk: Program Inconsistency Detection using Weakest Preconditions – Galois, Inc Presented by Aaron Tomb. Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior  often a collection of independent assertions sprinkled throughout the program. Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bugfinding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus. We have applied our analysis to a large body of widelyused opensource software, and found a number of bugs. 
Monday
Feb 7, 2011

Galois Tech talk: The Strategy Challenge in Computer Algebra – Galois, Inc Presented by Grant Passmore. In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: userspecifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different. In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worstcase doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one? The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification toolchains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions). 
Tuesday
Apr 12, 2011

Galois Tech Talk: The OpenTheory Standard Theory Library – Galois, Inc Presented by Joe Hurd. Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is crossprover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages. 
Tuesday
Jul 12, 2011

Galois tech talk: Parallel Kinduction based Model Checking – Galois, Inc Presented by Temesghen Kahsai. We give an overview of a parallel kinductionbased model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly messagebased, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic kinduction. A first level of parallelism is introduced in the kinduction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the kinduction loop as soon as they are produced and used to strengthen the induction hypothesis. This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property  valid or invalid  is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties. We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties. 
Wednesday
Aug 10, 2011

Galois tech talk: A MultiEncoding Approach for LTL Symbolic Satisfiability Checking – Galois, Inc Presented by Kristin Rozier Formal behavioral specifications written early in the systemdesign process and communicated across all design phases have been shown to increase the efficiency, consistency, and quality of the system under development. To prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. Our focus here is on specifications expressed in linear temporal logic (LTL). We introduce a novel encoding of symbolic transitionbased Buchi automata and a novel, ``sloppy,'' transition encoding, both of which result in improved scalability. We also define novel BDD variable orders based on tree decomposition of formula parse trees. We describe and extensively test a new multiencoding approach utilizing these novel encoding techniques to create 30 encoding variations. We show that our novel encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Details can be found here: http://ti.arc.nasa.gov/profile/kyrozier/. 
Tuesday
Aug 23, 2011

Tech Talk: Modular verification of preemptive OS kernels – Galois, Inc Presented by Alexey Gotsman Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK). 
Tuesday
Jan 10, 2012

Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework – Galois, Inc Presented by David Lazar Formal semantics is notoriously hard. The K semantic framework (http://kframework.org/) 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 nondeterminism 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 workinprogress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work. 
Wednesday
Jan 11, 2012

Galois Tech Talk (2 of 3 next week!): Modelbased Code Generation and Debugging of Concurrent Programs – Galois, Inc Presented by Borzoo Bonakdarpour. Design and implementation of distributed systems often involve many subtleties due to their complex structure, nondeterminism, 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 highlevel componentbased 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 multiparty strong synchronization primitives in atomic components by pointtopoint 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 multithreaded 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 dataflow 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 redblack trees) show significant performance improvement in optimallyinstrumented programs using our method as compared to adhoc overinstrumented programs. 
Thursday
Jan 12, 2012

Galois Tech Talk (3/3 next week!): On deadlock verification in microarchitectural models of communication fabrics. – Galois, Inc Presented by Julien Schmaltz. Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, microarchitectural models have been proposed as an efficient abstraction capturing the highlevel structure of designs. Microarchitectural 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 deadlockfree communication network combined with a deadlockfree protocol may have deadlocks or a system with a network with deadlocks combined with a deadlockfree protocol may be deadlockfree. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in microarchitectural 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 microarchitectures. 
Monday
Feb 6, 2012

Galois Tech Talk: Efficient Implementation of Property Directed Reachability – Galois, Inc Presented by Alan Mishchenko. Last spring, in March 2010, Aaron Bradley published the first truly new bitlevel 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. 
Thursday
Aug 30, 2012

Galois Tech Talk: Formal Verification of Monad Transformers – Galois, Inc Presented by Brian Huffman. We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with firstclass type constructors, firstclass polymorphism, or type quantification; instead, we rely on a domaintheoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes. 
Tuesday
Oct 16, 2012

Galois Tech Talk: Towards a Formally Verified Component Platform – Galois, Inc Presented by Matthew Fernandez. In safety and securitycritical environments software failures that are acceptable in other contexts may have expensive or even lifethreatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Componentbased development has the potential to lower the cost of systemwide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a componentbased development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation. 
Tuesday
Feb 12, 2013

Galois Tech Talk: Automatic Function Annotations for Hoare Logic – Galois, Inc Presented by Daniel Matichuk. Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a sidecondition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning. 
Tuesday
Mar 5, 2013

Galois Tech Talk: Parametricity, Quotient types, and Theorem transfer – Galois, Inc Presented by Brian Huffman. A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadlerstyle "free theorems" about a polymorphic function from its type; e.g. rev :: [a] > [a] must satisfy map f (rev xs) = rev (map f xs). In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using typesasbinaryrelations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types. 
Friday
Jun 14, 2013

Galois Tech Talk: Noninterference and Binary Correctness of seL4 – Galois, Inc Presented by Gerwin Klein and Thomas Sewell. This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code. The first part of the talk presents a new noninterference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain. The binary proof addresses the compilercorrectness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assemblylike programs powered by modern SMT solvers. We cover the previouslyverified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1. 
Tuesday
Jul 12, 2016

Galois Tech Talk: Hoare Monitor Programming Revisited : Safe and Optimized Concurrency – Galois, Inc abstract: Hoare monitors, invented by Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the HighAssurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, and how it is possible to improve runtime efficiency and parallelism of Towergenerated C programs by releasing some constraints on the Hoare monitor model. Finally, some test results on SMACCMPilot, a highassurance autopilot, will be presented. bio: GeorgesAxel Jaloyan is a CS student at École Normale Supérieure in Paris. He is interning at Galois as part of his Master’s degree. He is interested in embedded systems security and safetycritical systems. He interned previously at NASA Langley Safety Critical Avionics Systems Branch. 
Friday
Aug 3

Galois Tech Talk: The Lean Theorem Prover: Past, Present and Future – Galois Inc Abstract: Lean is an interactive theorem prover and functional programming language. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean has parallel compilation and checking of proofs, and provides a server mode that supports a continuous compilation and rich user interaction in editing environments such as Visual Studio Code, Monaco, Emacs, and Vim. In the first part of this talk, we provide a short introduction to Lean, its applications, and its metaprogramming framework. We also describe how this framework extends Lean’s object language with an API to many of Lean’s internal structures and procedures, and provides ways of reflecting objectlevel expressions into the metalanguage. We provide evidence to show that our implementation is efficient, and that it provides a convenient and flexible way of writing not only metaprograms and smallscale interactive tactics, but also more substantial kinds of automation. In the second part, we describe our plans for the system, and what we are currently working on. More information about Lean can be found at http://leanprover.github.io. The interactive book “Theorem Proving in Lean” is the standard reference for Lean. The book is available in PDF and HTML formats. In the HTML version, all examples and exercises can be executed in the reader’s web browser. Bio: I’m a Principal Researcher in the RiSE group at Microsoft Research. I joined Microsoft in 2006, before that I was a Computer Scientist at SRI International. I obtained my PhD at PUCRio in 2000. My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I’m the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is an open source theorem prover and programming language. Sebastian Ullrich and I are currently developing the next version (Lean 4). Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. Z3 has been open sourced (under the MIT license) in the beginning of 2015. I received the Haifa Verification Conference Award in 2010. In 2014, the TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) has given an award for “The most influential tool paper in the first 20 years of TACAS” to the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science. In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN. In 2017, the International Conference on Automated Deduction (CADE) presented the Skolem Award for my paper “Efficient EMatching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field. In 2018, the ETAPS conference has given the test of time award to the Z3 paper: Z3: An Efficient SMT Solver. You can see more about me at https://leodemoura.github.io/about.html 