BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:DAYLIGHT
DTSTART:20090308T020000
RDATE:20090308T020000
RDATE:20100314T020000
RDATE:20110313T020000
RDATE:20120311T020000
RDATE:20130310T020000
RDATE:20140309T020000
RDATE:20150308T020000
RDATE:20160313T020000
RDATE:20170312T020000
RDATE:20180311T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20091101T020000
RDATE:20091101T020000
RDATE:20101107T020000
RDATE:20111106T020000
RDATE:20121104T020000
RDATE:20131103T020000
RDATE:20141102T020000
RDATE:20151101T020000
RDATE:20161106T020000
RDATE:20171105T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20080921T221232Z
DTEND;VALUE=DATE:20081121
DTSTART;VALUE=DATE:20081117
DTSTAMP;VALUE=DATE-TIME:20080921T221232Z
LAST-MODIFIED;VALUE=DATE-TIME:20080922T155700Z
UID:http://calagator.org/events/1250455758
DESCRIPTION:This event runs from Monday\, November 17\, 2008 at 8:15am th
rough Thursday\, November 20\, 2008 at 3:45pm.\n\nDescription:\nImportan
t Dates
\;\n===============
\;\n Early Registration Deadline: Octo
ber 14\, 2008
\;\n Hotel Registration Deadline: October 18\, 2008
\;\n
\;\nConference Overview
\;\n===================
\;\n FMCAD
2008 is the eighth in a series of conferences on the theory
\;\n and
application of formal methods in hardware and system design and
\;\n
verification. In 2005\, the bi-annual FMCAD and sister conference
\;
\n CHARME decided to merge to form an annual conference with a unified&#
13\;\n community. The resulting unified FMCAD provides a leading
\;\n
international forum to researchers and practitioners in academia and
3\;\n industry for presenting and discussing groundbreaking methods\,
3\;\n technologies\, theoretical results\, and tools for formally reason
ing
\;\n about computing systems\, as well as open challenges therein
.
\;\n
\;\nLocal Information
\;\n=================
\;\n The
Conference will be held at the Embassy Suites (Downtown) in
\;\n Port
land\, Oregon. We have negotiated a special rate with the hotel
\;\n
for conference attendees. Please book early to secure the reduced
\
;\n rate. For details\, please see the conference web page. A dinner&#
13\;\n cruise on the Willamette River is planned.
\;\n
\;\nTechnic
al Program
\;\n=================
\;\n The technical program is ava
ilable at the conference web page. It
\;\n includes 2 invited keynot
es\, 4 invited tutorials\, 24 regular papers\,
\;\n 4 short papers\,
and 2 panels.
\;\n
\;\n Keynotes
\;\n --------
\;\n o Ken Mc
Millan (Cadence): Interpolation -- Theory and Applications
\;\n o Car
l Seger (Intel): Formal Methods and Physical Design: Match Made
\;\n
in Heaven or Fools' Paradise?
\;\n
\;\n Tutorials
\;\n ------
---
\;\n o Kevin Jones (Rambus): Analog and Mixed Signal Verification
: The
\;\n State of the Art and some Open Problems
\;\n o Moshe
Levinger (IBM): Building a Bridge: From Pre-Silicon
\;\n Verificati
on to Post-Silicon Validation
\;\n o Byron Cook (Microsoft): Computin
g Bounds on Space and Time for
\;\n Hardware Compilation.
\;\n o
David Hardin (Rockwell Collins): Considerations in the Design and
\;
\n Verification of Microprocessors for Safety-Critical and
\;\n S
ecurity-Critical Applications.
\;\n
\;\n Panels
\;\n ------
\;\n o High Level Design and ESL: Who Cares?
\;\n o The Future of For
mal: Academic\, IC\, EDA\, and Software Perspectives
\;\n
\;\nSpon
sors
\;\n========
\;\n Sponsored by: IEEE CEDA
\;\n In c
ooperation with: ACM SIGDA
\;\n Financial support: Cadence\, Galois
\, IBM\, Intel\, NEC\, Synopsys\n\nTags: fmcad\, formal methods\, hardwa
re\, ieee\, acm\n\nImported from: http://calagator.org/events/1250455758
URL:http://fmcad.org/2008
SUMMARY:FMCAD 2008 (Formal Methods in Computer Aided Design)
LOCATION:Embassy Suites Portland--Downtown: 319 Sw Pine St\, Portland OR
97204 US
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20091020T231649Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091027T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091027T103000
DTSTAMP;VALUE=DATE-TIME:20091020T231649Z
LAST-MODIFIED;VALUE=DATE-TIME:20091020T231649Z
UID:http://calagator.org/events/1250457887
DESCRIPTION:The next talk in the Galois Tech Seminar series:
\;\n
\
;\n * Date: Tuesday\, October 27th\, 2009
\;\n * Title: How to choose
between a screwdriver and a drill
\;\n * Speaker: Tanya L. Crenshaw&
#13\;\n * Time: 10:30am - 11:30am
\;\n * Location: Galois\, Inc. 421
SW 6th Ave. Suite 300\; Portland\, OR 97204
\;\n
\;\nFor details (
including an abstract and speaker bio)\, please see our
\;\nblog post
: http://www.galois.com/blog/2009/10/20/crenshaw-simplex/
\;\n
\;\
nAn RSVP is not required\; but feel free to drop a line to
\;\nlevent
.erkok@galois.com if you've any questions or comments.
\;\n
\;\nLe
vent Erkok\n\nTags: galois\, tech talk\, formal methods\, simplex\n\nImp
orted from: http://calagator.org/events/1250457887
URL:http://www.galois.com/blog/2009/10/20/crenshaw-simplex/
SUMMARY:Galois Talk: How to choose between a screwdriver and a drill
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20100129T230127Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100202T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100202T103000
DTSTAMP;VALUE=DATE-TIME:20100129T230127Z
LAST-MODIFIED;VALUE=DATE-TIME:20100129T230127Z
UID:http://calagator.org/events/1250458254
DESCRIPTION:Hello\,
\;\n
\;\nThe next Galois Tech Talk will be &quo
t\;An Introduction to the Maude Formal
\;\nTool Environment"\;\,
presented by Joe Hendrix on Tuesday\, February 2nd\,
\;\nat 10:30am.&
#13\;\n
\;\nFor more details\, please visit:
\;\nhttp://www.galois
.com/blog/2010/01/29/tech-talk-an-introduction-to-the-maude-formal-tool-
environment/
\;\n
\;\nHope to see you there!
\;\n-Iavor
\;\n
\n\nTags: formal methods\, functional programming\, galois\n\nImported f
rom: http://calagator.org/events/1250458254
URL:http://www.galois.com/blog/2010/01/29/tech-talk-an-introduction-to-th
e-maude-formal-tool-environment/
SUMMARY:Galois Tech Talk: "An Introduction to the Maude Formal Tool Envir
onment"
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20100521T214558Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100524T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100524T103000
DTSTAMP;VALUE=DATE-TIME:20100521T214558Z
LAST-MODIFIED;VALUE=DATE-TIME:20100521T214558Z
UID:http://calagator.org/events/1250458706
DESCRIPTION:The L4.verified Project
\;\nPresented by Dr. Gerwin Klein.
\;\n
\;\nLast year\, the NICTA L4.verifed project produced a form
al machine-checked Isabelle/HOL proof that the C code of the seL4 OS mic
rokernel correctly implements its abstract implementation. This talk wil
l give an overview of the proof together with its main implications and
assumptions\, and will show in which kinds of systems this formally veri
fied kernel can be used for gaining assurance on overall system security
.\n\nTags: formal methods\, functional programming\, galois\n\nImported
from: http://calagator.org/events/1250458706
URL:http://www.galois.com/blog/2010/05/21/tech-talk-the-l4-verified-proje
ct/
SUMMARY:Galois Tech Talk: The L4.verified Project
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20100611T222816Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100615T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100615T103000
DTSTAMP;VALUE=DATE-TIME:20100611T222816Z
LAST-MODIFIED;VALUE=DATE-TIME:20100611T222816Z
UID:http://calagator.org/events/1250458768
DESCRIPTION:Introducing Well-Founded Recursion
\;\nEric Mertens
\;\
n
\;\nImplementing recursive functions can be tricky when you want to
be certain that they eventually terminate. This talk introduces the con
cept of well-founded recursion as a tool for implementing recursive func
tions. It implements these concepts in the Agda programming language and
demonstrates the technique by implementing a simple version of Quicksor
t.\n\nTags: functional programming\, galois\, formal methods\n\nImported
from: http://calagator.org/events/1250458768
URL:http://www.galois.com/blog/2010/06/11/tech-talk-introducing-well-foun
ded-recursion/
SUMMARY:Galois Tech Talk: Introducing Well-Founded Recursion
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20101102T180305Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101109T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101109T103000
DTSTAMP;VALUE=DATE-TIME:20101102T180305Z
LAST-MODIFIED;VALUE=DATE-TIME:20101102T180344Z
UID:http://calagator.org/events/1250459418
DESCRIPTION:Presented by Lee Pike.
\;\n
\;\nWe address the problem
of runtime monitoring for hard real-time programs—a domain in which corr
ectness is critical yet has largely been overlooked in the runtime monit
oring community. We describe the challenges to runtime monitoring for th
is 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 str
eam-based dataflow language that generates small constant-time and const
ant-space C programs\, implementing embedded monitors. Copilot also gene
rates its own scheduler\, obviating the need for an underlying real-time
operating system. This talk will include fun pictures and videos.\n\nTa
gs: galois\, tech talk\, real time\, formal methods\n\nImported from: ht
tp://calagator.org/events/1250459418
URL:http://www.galois.com/blog/2010/11/02/tech-talk-copilot-a-hard-real-t
ime-runtime-monitor/
SUMMARY:Galois Tech Talk: Copilot: A Hard Real-Time Runtime Monitor
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20101109T220517Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101116T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101116T103000
DTSTAMP;VALUE=DATE-TIME:20101109T220517Z
LAST-MODIFIED;VALUE=DATE-TIME:20101109T220517Z
UID:http://calagator.org/events/1250459459
DESCRIPTION:speaker: Alwyn Goodloe
\;\n
\;\nCritical cyber-physical
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 foundat
ions\, but control engineers typically only work on Matlab/Simulink mode
ls\, ignoring the implementation all together. I will speak about an ong
oing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrow
ing this gap. I will briefly describe the design of a Matlab to C transl
ator being written in Haskell and verified using the Frama-C tool and th
e Prototype Verification System (PVS). In addition\, I will give a surve
y of our efforts in enhancing PVS’ capabilities in this area by building
a Linear Algebra library targeted at the math used by control engineers
.\n\nTags: galois\, tech talk\, control systems\, formal methods\n\nImpo
rted from: http://calagator.org/events/1250459459
URL:http://www.galois.com/blog/2010/11/09/tech-talk-formal-methods-applie
d-to-control-software/
SUMMARY:Galois Tech talk: Formal Methods Applied to Control Software
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110118T220744Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110125T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110125T103000
DTSTAMP;VALUE=DATE-TIME:20110118T220744Z
LAST-MODIFIED;VALUE=DATE-TIME:20110118T220744Z
UID:http://calagator.org/events/1250459650
DESCRIPTION:Presented by Aaron Tomb.
\;\n
\;\n 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 t
o work least well in the most common case: on large software systems tha
t have only partial specifications describing correct behavior --- often
a collection of independent assertions sprinkled throughout the program
.
\;\n
\;\nRecent research has suggested that a large class of sof
tware bugs fall into the category of inconsistencies\, or cases where tw
o pieces of program code make incompatible assumptions. Existing approac
hes to inconsistency detection have used intentionally unsound technique
s aimed at bug-finding rather than verification. In this dissertation\,
we describe an inconsistency detection analysis that subsumes previous w
ork and is instead based on the foundation of the weakest precondition c
alculus.
\;\n
\;\nWe have applied our analysis to a large body of
widely-used open-source software\, and found a number of bugs.\n\nTags:
galois\, tech talk\, formal methods\, static analysis\, debugging\n\nImp
orted from: http://calagator.org/events/1250459650
URL:http://corp.galois.com/blog/2011/1/18/tech-talk-program-inconsistency
-detection-using-weakest-prec.html
SUMMARY:Galois tech talk: Program Inconsistency Detection using Weakest P
reconditions
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110203T190905Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110207T173000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110207T163000
DTSTAMP;VALUE=DATE-TIME:20110203T190905Z
LAST-MODIFIED;VALUE=DATE-TIME:20110207T184533Z
UID:http://calagator.org/events/1250459721
DESCRIPTION:Presented by Grant Passmore.
\;\n
\;\nIn automated dedu
ction\, strategy is a vital ingredient in effective proof search. Strate
gy comes in many forms\, but the key is this: user-specifiable adaptatio
ns of general reasoning mechanisms reduce the search space by tailoring
its exploration to a particular class of problems. In fully automatic th
eorem provers\, this may happen through formula weights\, term orders an
d quantifier triggers. In interactive proof assistants\, one may build s
trategies by programming tactics and carefully crafting systems of rewri
te rules. Given that automated deduction often takes place over undecida
ble theories\, the recognition of a need for strategy is natural and hap
pened early in the field. In computer algebra\, the situation is rather
different.
\;\n
\;\nIn computer algebra\, the theories one works o
ver are often decidable but inherently infeasible. For instance\, the th
eory of real closed fields (i.e.\, nonlinear real arithmetic) is decidab
le\, but any full quantifier elimination algorithm for it is guaranteed
to have worst-case 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 com
es to practical applications\, is an infeasible theory really so differe
nt from an undecidable one?
\;\n
\;\nThe Strategy Challenge in Com
puter Algebra is this: To build theoretical and practical tools allowing
users to exert strategic control over the execution of core computer al
gebra algorithms. In this way\, such algorithms may be tailored to speci
fic 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 dis
sertation: (i) the theory of Abstract Groebner Bases and its use in deve
loping new Groebner basis algorithms tailored to the needs of SMT solver
s (joint with Leo de Moura)\, and (ii) the theory of Abstract Cylindrica
l Algebraic Decomposition and a family of real quantifier elimination al
gorithms tailored to the structure of nonlinear real arithmetic problems
arising in specific formal verification tool-chains. The former forms t
he foundation of nonlinear arithmetic in the SMT solver Z3\, and the lat
ter forms the basis of our tool RAHD (Real Algebra in High Dimensions).\
n\nTags: galois\, tech talk\, formal methods\, algebra\n\nImported from:
http://calagator.org/events/1250459721
URL:http://corp.galois.com/blog/2011/2/3/tech-talk-the-strategy-challenge
-in-computer-algebra.html
SUMMARY:Galois Tech talk: The Strategy Challenge in Computer Algebra
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110406T230025Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110412T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110412T103000
DTSTAMP;VALUE=DATE-TIME:20110406T230025Z
LAST-MODIFIED;VALUE=DATE-TIME:20110406T230025Z
UID:http://calagator.org/events/1250460443
DESCRIPTION:Presented by Joe Hurd.
\;\n
\;\nInteractive theorem pro
ving is tackling ever larger formalization and verification projects\, a
nd there is a critical need for theory engineering techniques to support
these efforts. One such technique is cross-prover package management\,
which has the potential to simplify the development of logical theories
and effectively share theories between different theorem prover implemen
tations. The OpenTheory project has developed standards for packaging th
eories of the higher order logic implemented by the HOL family of theore
m provers. What is currently missing is a standard theory library that c
an 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 o
f the HOL family of theorem provers\, and describe the process of instru
menting the HOL Light theorem prover to extract a standardized version o
f its core theory development. We profile the axioms and theorems of our
standard theory library and investigate the performance cost of separat
ing the standard theory library into coherent hierarchical theory packag
es.
\;\n\n\nTags: galois\, tech talk\, formal methods\, opentheory\n\
nImported from: http://calagator.org/events/1250460443
URL:http://corp.galois.com/blog/2011/4/6/tech-talk-the-opentheory-standar
d-theory-library.html
SUMMARY:Galois Tech Talk: The OpenTheory Standard Theory Library
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110705T174842Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110712T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110712T103000
DTSTAMP;VALUE=DATE-TIME:20110705T174842Z
LAST-MODIFIED;VALUE=DATE-TIME:20110705T174842Z
UID:http://calagator.org/events/1250460798
DESCRIPTION:Presented by Temesghen Kahsai.
\;\n
\;\nWe give an over
view of a parallel k-induction-based model checking architecture for ver
ifying safety properties of synchronous systems. The architecture\, whic
h is strictly message-based\, is designed to minimize synchronization de
lays and easily accommodate the incorporation of incremental invariant g
enerators to enhance basic k-induction. A first level of parallelism is
introduced in the k-induction 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 gen
erate invariants for the system being verified. The invariants are fed t
o the k-induction loop as soon as they are produced and used to strength
en the induction hypothesis.
\;\n
\;\nThis architecture allows the
verification of multiple properties in an incremental fashion. Specific
ally\, the outcome of a property -- valid or invalid -- is communicated
to the user as soon as the result is known. Moreover\, verified valid pr
operties are added as invariants in the model checking procedure to aid
the verification of the remaining properties.
\;\n
\;\nWe provide
experimental evidence that this incremental and parallel architecture si
gnificantly speeds up the verification of safety properties. Additionall
y\, due to the automatic invariant generation\, it also considerably inc
reases the number of provable safety properties.\n\nTags: galois\, tech
talk\, formal methods\, model checking\n\nImported from: http://calagato
r.org/events/1250460798
URL:http://corp.galois.com/blog/2011/7/5/tech-talk-parallel-k-induction-b
ased-model-checking.html
SUMMARY:Galois tech talk: Parallel K-induction based Model Checking
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110808T162902Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110810T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110810T103000
DTSTAMP;VALUE=DATE-TIME:20110808T162902Z
LAST-MODIFIED;VALUE=DATE-TIME:20110808T162902Z
UID:http://calagator.org/events/1250461200
DESCRIPTION:Presented by Kristin Rozier
\;\n
\;\nFormal behavioral
specifications written early in the system-design
\;\nprocess and com
municated across all design phases have been shown to
\;\nincrease th
e efficiency\, consistency\, and quality of the system under
\;\ndev
elopment. To prevent introducing design or verification errors\, it is&#
13\;\ncrucial to test specifications for satisfiability. Our focus here
is on
\;\nspecifications expressed in linear temporal logic (LTL).
3\;\n
\;\nWe introduce a novel encoding of symbolic transition-based
Buchi
\;\nautomata and a novel\, ``sloppy\,'' transition encoding\, b
oth of which
\;\nresult in improved scalability. We also define nove
l BDD variable
\;\norders based on tree decomposition of formula pars
e trees. We describe
\;\nand extensively test a new multi-encoding ap
proach utilizing these novel
\;\nencoding techniques to create 30 enc
oding variations. We show that our
\;\nnovel encodings translate to s
ignificant\, sometimes exponential\,
\;\nimprovement over the current
standard encoding for symbolic LTL
\;\nsatisfiability checking.
\
;\n
\;\nDetails can be found here: http://ti.arc.nasa.gov/profile/kyr
ozier/.\n\nTags: galois\, tech talk\, formal methods\n\nImported from: h
ttp://calagator.org/events/1250461200
URL:http://corp.galois.com/blog/2011/8/8/tech-talk-a-multi-encoding-appro
ach-for-ltl-symbolic-satisfi.html
SUMMARY:Galois tech talk: A Multi-Encoding Approach for LTL Symbolic Sati
sfiability Checking
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110819T221826Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110823T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110823T103000
DTSTAMP;VALUE=DATE-TIME:20110819T221826Z
LAST-MODIFIED;VALUE=DATE-TIME:20110822T142933Z
UID:http://calagator.org/events/1250461233
DESCRIPTION:Presented by Alexey Gotsman
\;\n
\;\nMost major OS kern
els today run on multiprocessor systems and are preemptive: it is possib
le for a process running in the kernel mode to get descheduled. Existing
modular techniques for verifying concurrent code are not directly appli
cable in this setting: they rely on scheduling being implemented correct
ly\, and in a preemptive kernel\, the correctness of the scheduler is in
terdependent with the correctness of the code it schedules. This interde
pendency is even stronger in mainstream kernels\, such as Linux\, FreeBS
D or XNU\, where the scheduler and processes interact in complex ways. I
n this talk I will present the first logic that is able to decompose th
e verification of preemptive multiprocessor kernel code into verifying t
he scheduler and the rest of the kernel separately\, even in the presenc
e of complex interdependencies between the two components present in mai
nstream kernels. This is joint work with Hongseok Yang (University of Ox
ford\, UK).\n\nTags: tech talk\, galois\, formal methods\n\nImported fro
m: http://calagator.org/events/1250461233
URL:https://corp.galois.com/blog/2011/8/19/tech-talk-modular-verification
-of-preemptive-os-kernels.html
SUMMARY:Tech Talk: Modular verification of preemptive OS kernels
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120103T181917Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T103000
DTSTAMP;VALUE=DATE-TIME:20120103T181917Z
LAST-MODIFIED;VALUE=DATE-TIME:20120103T181917Z
UID:http://calagator.org/events/1250461795
DESCRIPTION:Presented by David Lazar
\;\n
\;\nFormal semantics is n
otoriously hard. The K semantic framework (http://k-framework.org/) is a
system that makes the task of formally defining programming languages e
asy 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 co
rrectness. These features made it possible to develop a complete formal
semantics of the C language in K.
\;\nThe 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 gui
ding example. The second half of the talk will focus on a work-in-progre
ss formalization of Haskell 98 in K. We'll look at the challenges of for
malizing Haskell and the applications of this work.\n\nTags: galois\, ha
skell\, formal methods\, tech talk\, semantics\n\nImported from: http://
calagator.org/events/1250461795
URL:https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-we
ek-formalizing-haskell-98-in.html
SUMMARY:Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in t
he K Semantic Framework
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120104T213843Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120111T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120111T103000
DTSTAMP;VALUE=DATE-TIME:20120104T213843Z
LAST-MODIFIED;VALUE=DATE-TIME:20120104T213843Z
UID:http://calagator.org/events/1250461800
DESCRIPTION:Presented by Borzoo Bonakdarpour.
\;\n
\;\nDesign and i
mplementation of distributed systems often involve many subtleties due t
o their complex structure\, non-determinism\, and low atomicity as well
as occurrence of unanticipated physical events such as faults. Thus\, co
nstructing correct distributed systems has always been a challenge and o
ften subject to serious errors. We propose a method for generating distr
ibuted implementations from high-level component-based models that only
employ simple synchronization primitives. The method is a sequence of th
ree transformations preserving observational equivalence: (1) A transfor
mation from a global state to a partial state model\, (2) a transformati
on which replaces multi-party strong synchronization primitives in atomi
c components by point-to-point send/receive primitives based on asynchro
nous message passing\, and (3) a final transformation to concrete distri
buted implementation based on platform and architecture. We study the pr
operties of different transformations\, in particular\, performance crit
eria such as degree of parallelism and overhead for coordination.
\;\
n
\;\nThe second part of the talk will focus on an automated techniqu
e for optimal instrumentation of multi-threaded programs for debugging a
nd testing of concurrent data structures. We define a notion of observab
ility that enables debuggers to trace back and locate errors through dat
a-flow instrumentation. Observability in a concurrent program enables a
debugger to extract the value of a set of desired variables through inst
rumenting another (possibly smaller) set of variables. We formulate an o
ptimization problem that aims at minimizing the size of the latter set.
Our experimental results on popular concurrent data structures (e.g.\, l
inked lists and red-black trees) show significant performance improvemen
t in optimally-instrumented programs using our method as compared to ad-
hoc over-instrumented programs.\n\nTags: galois\, formal methods\, tech
talk\, concurrency\n\nImported from: http://calagator.org/events/1250461
800
URL:https://corp.galois.com/blog/2012/1/4/galois-tech-talk-2-of-3-next-we
ek-model-based-code-generatio.html
SUMMARY:Galois Tech Talk (2 of 3 next week!): Model-based Code Generation
and Debugging of Concurrent Programs
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120106T012427Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120112T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120112T103000
DTSTAMP;VALUE=DATE-TIME:20120106T012427Z
LAST-MODIFIED;VALUE=DATE-TIME:20120106T012427Z
UID:http://calagator.org/events/1250461808
DESCRIPTION:Presented by Julien Schmaltz.
\;\n
\;\nCommunication fa
brics constitute an important challenge for the design and verification
of multicore architectures. To enable their formal analysis\, micro-arch
itectural models have been proposed as an efficient abstraction capturin
g the high-level structure of designs. Micro-architectural models also i
nclude 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 combin
ation: 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-fr
ee. This combination also makes the verification problem more complicate
d. We will present an algorithm for efficient deadlock verification in m
icro-architectural models. We will discuss the limitations of this appro
ach and point to future research direction. An important future applicat
ion of our methodology is the verification of cache coherency at the lev
el of micro-architectures.\n\nTags: galois\, formal methods\, hardware\,
tech talk\, verification\n\nImported from: http://calagator.org/events/
1250461808
URL:https://corp.galois.com/blog/2012/1/5/galois-tech-talk-33-next-week-o
n-deadlock-verification-in-mi.html
SUMMARY:Galois Tech Talk (3/3 next week!): On deadlock verification in mi
cro-architectural models of communication fabrics.
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120201T015730Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120206T110000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120206T100000
DTSTAMP;VALUE=DATE-TIME:20120201T015730Z
LAST-MODIFIED;VALUE=DATE-TIME:20120201T015730Z
UID:http://calagator.org/events/1250461916
DESCRIPTION:Presented by Alan Mishchenko.
\;\n
\;\nLast spring\, in
March 2010\, Aaron Bradley published the first truly new bit-level symb
olic model checking algorithm since Ken McMillan’s interpolation based m
odel checking procedure introduced in 2003. Our experience with the algo
rithm suggests that it is stronger than interpolation on industrial prob
lems\, and that it is an important algorithm to study further. In this p
aper\, we present a simplified and faster implementation of Bradley’s pr
ocedure\, and discuss our successful and unsuccessful attempts to improv
e it.\n\nTags: galois\, formal methods\, tech talk\, model checking\n\nI
mported from: http://calagator.org/events/1250461916
URL:http://corp.galois.com/blog/2012/1/31/tech-talk-efficient-implementat
ion-of-property-directed-reac.html
SUMMARY:Galois Tech Talk: Efficient Implementation of Property Directed R
eachability
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120824T170527Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120830T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120830T110000
DTSTAMP;VALUE=DATE-TIME:20120824T170527Z
LAST-MODIFIED;VALUE=DATE-TIME:20120824T170527Z
UID:http://calagator.org/events/1250462780
DESCRIPTION:Presented by Brian Huffman.
\;\n
\;\nWe present techniq
ues for reasoning about constructor classes that (like the monad class)
fix polymorphic operations and assert polymorphic axioms. We do not requ
ire a logic with first-class type constructors\, first-class polymorphis
m\, or type quantification\; instead\, we rely on a domain-theoretic mod
el of the type system in a universal domain to provide these features. T
hese 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 w
riter transformers do not universally preserve the monad laws\; however\
, we establish datatype invariants for each\, showing that they are vali
d monads when viewed as abstract datatypes.\n\nTags: galois\, functional
programming\, haskell\, formal methods\, tech talk\, Isabelle\n\nImport
ed from: http://calagator.org/events/1250462780
URL:https://corp.galois.com/blog/2012/8/24/tech-talk-formal-verification-
of-monad-transformers.html
SUMMARY:Galois Tech Talk: Formal Verification of Monad Transformers
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20121009T165835Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T103000
DTSTAMP;VALUE=DATE-TIME:20121009T165835Z
LAST-MODIFIED;VALUE=DATE-TIME:20121009T165835Z
UID:http://calagator.org/events/1250462942
DESCRIPTION:Presented by Matthew Fernandez.
\;\n
\;\nIn safety- and
security-critical environments software failures that are acceptable in
other contexts may have expensive or even life-threatening consequences
. Formal verification has the potential to provide high assurance for th
is software\, but is regarded as being prohibitively expensive. Although
significant advances have been made in this area\, verification of larg
er systems still remains impractical. Component-based development has th
e potential to lower the cost of system-wide verification\, bringing cor
rectness proofs of these large scale systems within reach. This talk wil
l discuss my work that aims to provide a component-based development env
ironment for building systems with high assurance requirements. By provi
ding a formal model of the platform with proven correctness properties t
hat hold at the level of an abstract model right down to the implementat
ion\, I hope to reduce the cost of full system verification by allowing
reasoning about system components in isolation.
\;\n\n\nTags: galois\
, formal methods\, tech talk\, l4\, OS design\, kernels\n\nImported from
: http://calagator.org/events/1250462942
URL:https://corp.galois.com/blog/2012/10/9/tech-talk-towards-a-formally-v
erified-component-platform.html
SUMMARY:Galois Tech Talk: Towards a Formally Verified Component Platform
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20130206T180129Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130212T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130212T103000
DTSTAMP;VALUE=DATE-TIME:20130206T180129Z
LAST-MODIFIED;VALUE=DATE-TIME:20130206T180129Z
UID:http://calagator.org/events/1250463528
DESCRIPTION:Presented by Daniel Matichuk.
\;\n
\;\nFormal verifica
tion can provide a high degree of assurance for critical software\, but
can come at the cost of large artefacts that must be maintained alongsid
e it. When using an interactive theorem prover\, these artefacts take th
e 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 i
ntermediate program states to be easily reused. Program functions are an
notated with properties as a side-condition of existing proofs. These an
notations can reduce the proof burden substantially when subsequent prog
ram properties need to be shown. Implemented in Isabelle\, it is shown t
o be practically useful by greatly simplifying cases where existing proo
fs contained largely duplicated reasoning.\n\nTags: galois\, formal meth
ods\, tech talk\n\nImported from: http://calagator.org/events/1250463528
URL:https://corp.galois.com/blog/2013/2/6/tech-talk-automatic-function-an
notations-for-hoare-logic.html
SUMMARY:Galois Tech Talk: Automatic Function Annotations for Hoare Logic
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20130301T020956Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130305T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130305T103000
DTSTAMP;VALUE=DATE-TIME:20130301T020956Z
LAST-MODIFIED;VALUE=DATE-TIME:20130301T020956Z
UID:http://calagator.org/events/1250463749
DESCRIPTION:Presented by Brian Huffman.
\;\n
\;\nA polymorphic func
tion may be instantiated at many different types\; if the function is pa
rametrically polymorphic\, then all of its instances must behave uniform
ly. Reynolds' parametricity theorem expresses this precisely\, in terms
of binary relations derived from types. One application of the parametri
city theorem is to derive Wadler-style "\;free theorems"\; about
a polymorphic function from its type\; e.g. rev :: [a] ->\; [a] must
satisfy map f (rev xs) = rev (map f xs).
\;\n
\;\nIn 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
types-as-binary-relations\, we can automatically prove that correspondin
g propositions about quotient types and their representation types are l
ogically equivalent. This design is implemented as the Transfer package
in the Isabelle theorem prover\, where it is used to automate many proof
s about quotient types.\n\nTags: galois\, formal methods\, tech talk\n\n
Imported from: http://calagator.org/events/1250463749
URL:https://corp.galois.com/blog/2013/2/28/tech-talk-parametricity-quotie
nt-types-and-theorem-transfer.html
SUMMARY:Galois Tech Talk: Parametricity\, Quotient types\, and Theorem tr
ansfer
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20130607T010656Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130614T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130614T110000
DTSTAMP;VALUE=DATE-TIME:20130607T010656Z
LAST-MODIFIED;VALUE=DATE-TIME:20130607T010656Z
UID:http://calagator.org/events/1250464379
DESCRIPTION:Presented by Gerwin Klein and Thomas Sewell.
\;\n
\;\nT
his talk introduces two new facets that have recently been added to the
seL4 formal verification story: a proof the kernel does not leak informa
tion between domains\, and a proof that the compiled binary matches the
expected semantics of the C source code.
\;\n
\;\nThe first part o
f the talk presents a new non-interference theorem for seL4\, which buil
ds on the earlier function correctness verification. The theorem shows h
ow seL4 can be configured as a static separation kernel with dynamic ker
nel services within each domain.
\;\n
\;\nThe binary proof address
es the compiler-correctness assumption of the earlier seL4 proofs by con
necting the compiled binary to the refinement chain\, thus showing that
the seL4 binary used in practice has all of the properties that have bee
n shown of its models. We use the Cambridge ARM model and Magnus Myreen'
s certifying decompiler\, together with a custom correspondence finder f
or assembly-like programs powered by modern SMT solvers. We cover the pr
eviously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisati
on level 1.\n\nTags: galois\, formal methods\, tech talk\, kernels\n\nIm
ported from: http://calagator.org/events/1250464379
URL:http://corp.galois.com/blog/2013/6/6/tech-talk-non-interference-and-b
inary-correctness-of-sel4.html
SUMMARY:Galois Tech Talk: Non-interference and Binary Correctness of seL4
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20160707T154107Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160712T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160712T110000
DTSTAMP;VALUE=DATE-TIME:20160707T154107Z
LAST-MODIFIED;VALUE=DATE-TIME:20160707T154107Z
UID:http://calagator.org/events/1250470541
DESCRIPTION:abstract:
\;\n
\;\nHoare monitors\, invented by Hansen
and Hoare in 1973\, are widely used to safely handle concurrent programm
ing in different languages ranging from C++11 to Tower\, an EDSL develop
ed by Galois as part of the High-Assurance 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 efficien
cy and parallelism of Tower-generated C programs by releasing some const
raints on the Hoare monitor model. Finally\, some test results on SMACCM
Pilot\, a high-assurance autopilot\, will be presented.
\;\n
\;\nb
io:
\;\n
\;\nGeorges-Axel 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 safety-critica
l systems. He interned previously at NASA Langley Safety Critical Avioni
cs Systems Branch.\n\nTags: Galois tech talk\, concurrency\, formal meth
ods\n\nImported from: http://calagator.org/events/1250470541
URL:https://galois.com/blog/2016/07/tech-talk-hoare-monitor-programming-r
evisited-safe-optimized-concurrency/
SUMMARY:Galois Tech Talk: Hoare Monitor Programming Revisited : Safe and
Optimized Concurrency
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20180724T220828Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180803T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180803T110000
DTSTAMP;VALUE=DATE-TIME:20180724T220828Z
LAST-MODIFIED;VALUE=DATE-TIME:20180724T220828Z
UID:http://calagator.org/events/1250474036
DESCRIPTION:Abstract:
\;\nLean is an interactive theorem prover and fu
nctional programming language. Lean implements a version of the Calculus
of Inductive Constructions. Its elaborator and unification algorithms a
re designed around the use of type classes\, which support algebraic rea
soning\, programming abstractions\, and other generally useful means of
expression. Lean has parallel compilation and checking of proofs\, and p
rovides a server mode that supports a continuous compilation and rich us
er interaction in editing environments such as Visual Studio Code\, Mona
co\, Emacs\, and Vim. In the first part of this talk\, we provide a shor
t introduction to Lean\, its applications\, and its metaprogramming fram
ework. We also describe how this framework extends Lean’s object languag
e with an API to many of Lean’s internal structures and procedures\, and
provides ways of reflecting object-level expressions into the metalangu
age. We provide evidence to show that our implementation is efficient\,
and that it provides a convenient and flexible way of writing not only m
etaprograms and small-scale interactive tactics\, but also more substant
ial kinds of automation. In the second part\, we describe our plans for
the system\, and what we are currently working on.
\;\n
\;\nMore i
nformation about Lean can be found at http://leanprover.github.io. The i
nteractive 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 browse
r.
\;\n
\;\nBio:
\;\nI’m a Principal Researcher in the RiSE gro
up at Microsoft Research. I joined Microsoft in 2006\, before that I was
a Computer Scientist at SRI International. I obtained my PhD at PUC-Rio
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 programmin
g language. Sebastian Ullrich and I are currently developing the next ve
rsion (Lean 4). Z3 and Yices are SMT solvers\, and SAL (the Symbolic Ana
lysis Laboratory) is an open source tool suite that includes symbolic an
d bounded model checkers\, and automatic test generators. Z3 has been op
en sourced (under the MIT license) in the beginning of 2015. I received
the Haifa Verification Conference Award in 2010. In 2014\, the TACAS con
ference (Tools and Algorithms for the Construction and Analysis of Syste
ms) 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 I
nternational Conference\, TACAS 2008\, vol. 4963 of Lecture Notes in Com
puter Science. In 2015\, Z3 received the Programming Languages Software
Award from ACM SIGPLAN. In 2017\, the International Conference on Automa
ted Deduction (CADE) presented the Skolem Award for my paper “Efficient
E-Matching for SMT Solvers” that has passed the test of time\, by being
a most influential paper in the field. In 2018\, the ETAPS conference ha
s given the test of time award to the Z3 paper: Z3: An Efficient SMT Sol
ver. You can see more about me at https://leodemoura.github.io/about.htm
l\n\nTags: lean\, theorem proving\, computer science\, formal methods\n\
nImported from: http://calagator.org/events/1250474036
URL:https://galois.com/blog/2018/07/the-lean-theorem-prover-past-present-
and-future/
SUMMARY:Galois Tech Talk: The Lean Theorem Prover: Past\, Present and Fut
ure
LOCATION:Galois Inc: 421 Sw 6th Ave Ste 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR