Abstract QuickCheck is a powerful library for automatic test-case generation. Because QuickCheck performs random testing, some of the counterexamples discovered are very large. QuickCheck provides an interface for the user to write shrink functions to attempt to reduce the size of counterexamples. Hand-written implementations of shrink can be complex, inefficient, and consist of significant boilerplate […]

Abstract C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic […]

abstract: How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional “design+verify” approach to “specify+synthesize” in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that […]

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 that this talk is on Friday, at 11am title:Non-interference and Binary Correctness of seL4 speaker:Gerwin Klein and Thomas Sewell, NICTA time: Friday, 14 June 2013, […]

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: Automatic Function Annotations for Hoare Logic speaker: Daniel Matichuk time: Tuesday, 12 February 2013, 10:30am. location: Galois Inc. 421 SW 6th Ave. Suite 300, Portland, OR, […]

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: Towards a Formally Verified Component Platform speaker: Matthew Fernandez time: Tuesday, 16 October 2012, 10:30am location: Galois Inc. 421 SW 6th Ave. Suite 300, Portland, OR, […]

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: […]

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 […]

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, 15 December 2011. title: Frenetic: A Network Programming Language speaker: Nate Foster time: Thursday, 15 […]

Galois is pleased to host the following back-to-back tech talks.These talks are open to the interested public. Please join us! speakers:Sebastian Niller and Nis N. Wegmann time:16 August 2011, Tuesday, 10:30 A.M. location:Galois, Inc.421 SW 6th AveSte 300Portland, OR 97204(3rd floor of the Commonwealth building)   #1 title:Translation of Functionally Embedded Domain-specific Languages With Static Type […]