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