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:20080309T020000 RDATE:20080309T020000 RDATE:20090308T020000 RDATE:20100314T020000 RDATE:20110313T020000 RDATE:20120311T020000 RDATE:20130310T020000 RDATE:20140309T020000 RDATE:20150308T020000 RDATE:20160313T020000 RDATE:20170312T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT BEGIN:STANDARD DTSTART:20081102T020000 RDATE:20081102T020000 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:20080711T231204Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080715T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080715T103000 DTSTAMP;VALUE=DATE-TIME:20080711T231204Z LAST-MODIFIED;VALUE=DATE-TIME:20080713T043231Z UID:http://calagator.org/events/1250455508 DESCRIPTION:Just a quick note about next week's Galois Tech Talk. Now tha t Galois has completed its move into downtown Portland\, and a shiny new \, centrally located\, office space\, we're opening up our tech talk ser ies a bit more widely. If you're in Portland\, and interested in functi onal programming and formal methods\, drop by! \;\n \;\n--------- --------------------------------------------------------------- \;\n \;\nTITLE: Stream Fusion for Haskell Arrays \;\n \;\nspe aker: Don Stewart \;\nDATE: Tuesday\, July 15th\, 10.30am s harp. \;\n \;\nLOCATION: \;\nGalois\, Inc. \;\n421 SW 6 th Ave. Suite 300 \;\n(3rd floor of the Commonwealth Building) \ ;\nPortland\, Oregon \;\n \;\nABSTRACT: \;\n \;\nArrays ha ve traditionally been an awkward data structure for Haskell programmers. Despite the large number of array libraries available\, they have remai ned relatively awkward to use in comparison to the rich suite of purely functional data structures\, such as fingertrees or finite maps. Arrays have simply not been first class citizens in the language. \;\n \ ;\nIn this talk we'll begin with a survey of the more than a dozen array types available\, including some new matrix libraries developed in the past year. I'll then describe a new efficient\, pure\, and flexible arra y library for Haskell with a list like interface\, based on work in the Data Parallel Haskell project\, that employs stream fusion to dramatical ly reduce the cost of pure arrays. The implementation will be presented from the ground up\, along with a discussion of the entire compilation p rocess of the library\, from source to assembly. \;\n \;\nABOUT T HE GALOIS TECH TALKS: \;\n \;\nGalois (http://galois.com) has been holding weekly technical seminars for several years on topics from func tional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system construction\, with talks by many fi gures from the programming language and formal methods communities. \;\n \;\nThe talks are open and free. If you're planning to attend\, dropping a note to is appreciated\, but not required. If you're interes ted in giving a talk\, Don's always looking for new speakers. \;\n\n\ nImported from: http://calagator.org/events/1250455508 URL:http://groups.google.com/group/pdxfunc/browse_thread/thread/c15f41f7d 4379186 SUMMARY:Galois Tech Talk: Don Stewart\, "Stream Fusion for Haskell Arrays " LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080817T213401Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080819T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080819T103000 DTSTAMP;VALUE=DATE-TIME:20080817T213401Z LAST-MODIFIED;VALUE=DATE-TIME:20080817T213401Z UID:http://calagator.org/events/1250455632 DESCRIPTION:Title: Adventures in Foreign Function Interfaces \;\n \;\nSpeaker: Joel Stanley \;\n Galois\, Inc. \;\ n \;\nDate: Tuesday\, August 19th\, 10.30am \;\n \;\nLoca tion: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \; \n (3rd floor of the Commonwealth Building) \;\n Portland\, Oregon \;\n \;\nAbstract: \;\n \;\n In-proce ss integration and data exchange between multiple language \;\n ru ntimes is a classic software engineering challenge. This talk \;\n describes our experiences in building an open-source tool for \;\n generating an "\;FFI bridge"\; between Poly/ML and OCaml\, vi a the common \;\n C FFI provided by both language's runtimes. \ ;\n \;\n The first intended use of this tool is to programmaticall y generate \;\n a bridge between Isabelle (on the Poly/ML side) an d Intel's Decision \;\n Procedure Toolkit API (on the OCaml side). \;\n \;\nAbout the Galois Tech Talks. \;\n \;\n Galois ( http://galois.com) has been holding weekly technical \;\n seminars for several years on topics from functional programming\, \;\n fo rmal methods\, compiler and language design\, to cryptography\, and \ ;\n operating system construction\, with talks by many figures from t he \;\n programming language and formal methods communities. \; \n \;\n The talks are open and free. If you're planning to attend\ , dropping \;\n a note to is appreciated\, but not required. \ ;\n If you're interested in giving a talk\, we're always looking for new \;\n speakers. \n\nTags: galois\, functional programming\n\nIm ported from: http://calagator.org/events/1250455632 URL:http://groups.google.com/group/pdxfunc/browse_thread/thread/21d166d2c 615874c SUMMARY:Galois Tech Talk: Adventures in Foreign Function Interfaces LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080823T074326Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080827T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080827T103000 DTSTAMP;VALUE=DATE-TIME:20080823T074326Z LAST-MODIFIED;VALUE=DATE-TIME:20080823T074354Z UID:http://calagator.org/events/1250455655 DESCRIPTION:TOPIC: \;\nLarge Scale Monadic Refinement - Tales from L4. verified \;\n \;\nSPEAKER: \;\nThomas Sewell\, NICTA \;\n&# 13\;\nDATE: \;\n**Wednesday** \, August 27th\, 10.30am \;\n \; \nLOCATION: \;\nGalois\, Inc. \;\n421 SW 6th Ave. Suite 300 \; \n(3rd floor of the Commonwealth Building) \;\nPortland\, Oregon \ ;\n \;\nABSTRACT: \;\nComponents of operating systems have emerged as an attractive target for formal analysis\, thanks to the key importa nce of operating system correctness in establishing the security of a ra nge of applications. These systems present a number of unique challenges for analysis\, including their low level implementation and their detai led view of the system state. This talk will address none of these\, ins tead focusing on the challenges of reasoning about (relatively) large\, non-modular\, inherently imperative software artefacts. \;\n \;\nT he talk will describe the formalisation of the seL4 microkernel using a state monad with nondeterminism and exceptions\, present a refinement an d Hoare calculus\, and discuss the impact of this chosen approach on the effectiveness of the overall verification effort. \;\n \;\nBIOGRA PHICAL DETAILS: \;\nThomas Sewell is a software engineer with an inte rest in pure mathematics. He obtained his BE &\; BSc from UNSW in 200 6\, and has been working as a proof engineer for NICTA's L4.verified pro ject for two and a half years. \;\n \;\nABOUT THE GALOIS TECH TALK S. \;\nGalois (http://galois.com) has been holding weekly technical s eminars for several years on topics from functional programming\, formal methods\, compiler and language design\, to cryptography\, and operatin g system construction\, with talks by many figures from the programming language and formal methods communities. \;\n \;\nThe talks are op en and free. If you're planning to attend\, dropping a note to is appre ciated\, but not required. If you're interested in giving a talk\, we're always looking for new speakers. \;\n\n\nImported from: http://calag ator.org/events/1250455655 URL:http://groups.google.com/group/pdxfunc/browse_thread/thread/40a178872 a66bdb3 SUMMARY:Large Scale Monadic Refinement - Tales from L4.verified LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080829T185647Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080902T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080902T103000 DTSTAMP;VALUE=DATE-TIME:20080829T185647Z LAST-MODIFIED;VALUE=DATE-TIME:20080829T185647Z UID:http://calagator.org/events/1250455662 DESCRIPTION: \;\nTitle: GpuGen: Bringing the Power of GPUs into t he Haskell World \;\n \;\nSpeaker: Sean Lee \;\n P rogramming Languages &\; Systems \;\n UNSW\, Sydney \ ;\n \;\nDate: Tuesday\, September 2nd. \;\n 10.30a m \;\n \;\nLocation: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \;\n (3rd floor of the Commonwealth Building ) \;\n Portland\, Oregon \;\n \;\nAbstract: \;\n&# 13\;\nFor the last decade\, the performance of GPUs has out-grown CPUs\, and \;\ntheir programmability has also improved to the level where t hey can be \;\nused fo general-purpose computations. Nonetheless\, GP U programming is \;\nstill limited only to those who understand the h ardware architecture and \;\nthe parallel processing. This is because the current GPU programming \;\nsystems are based on the specialized parallel processing model\, and \;\nrequire low-level attention in m any aspects such as thread launching \;\nand synchronization. \;\n \;\nThe need for a programming system which provides a high-level 3\;\nabstraction layer on top of the GPU programming systems without los ing \;\nthe performance gain arises to facilitate the use of GPUs. In stead of \;\nwriting a programming system from the scratch\, the deve lopment of a \;\nHaskell extension has been chosen as the ideal appro ach\, since the \;\nHaskell community has already accumulated a signi ficant amount of \;\nresearch and resources for Nested Data Paralleli sm\, which could be \;\nadopted to provide a high-level abstraction o n GPU programming and even \;\nto broaden the applicability of GPU pr ogramming. In addition\, the \;\nForeign Function Interface of Haskel l is sufficient to be the \;\ncommunication medium to the GPU. \;\ n \;\nGpuGen is what connects these two dots: GPUs and Haskell. It co mpiles \;\nthe collective data operations such as scan\, fold\, map\, etc\, which \;\nincur most computation cost\, to the GPU. The design of the system\, the \;\nstructure of the GpuGen compiler\, and the c urrent development status are \;\nto be discussed in the talk. \;\ n \;\nBiographical details: \;\n \;\n Sean Lee is a PhD candi date at the UNSW\, Sydney\, working \;\n in the Programming Languag es &\; Systems Group. This summer \;\n he's been interning at Nv idia in Santa Clara\, working on \;\n programming GPUs with Haskell . \;\n \;\nAbout the Galois Tech Talks. \;\n \;\n Galois ( http://galois.com) has been holding weekly technical \;\n seminars for several years on topics from functional programming\, \;\n form al methods\, compiler and language design\, to cryptography\, and \;\ n operating system construction\, with talks by many figures from the& #13\;\n programming language and formal methods communities. \;\n&# 13\;\n The talks are open and free. If you're planning to attend\, dro pping \;\n a note to is appreciated\, but not required. \;\n If you're interested in giving a talk\, we're always looking for new \;\n speakers.\n\nTags: galois\, technology\, functional programming\, pdxfunc\n\nImported from: http://calagator.org/events/1250455662 URL:http://groups.google.com/group/pdxfunc/browse_thread/thread/33da952d0 02bb1c7 SUMMARY:Galois Tech Talk: GpuGen: Bringing the Power of GPUs into the Has kell World LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080904T101231Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080909T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080909T103000 DTSTAMP;VALUE=DATE-TIME:20080904T101231Z LAST-MODIFIED;VALUE=DATE-TIME:20080904T101255Z UID:http://calagator.org/events/1250455680 DESCRIPTION:TITLE: \;\nPretty-Printing a Really Long Formula (or\, &qu ot\;What a Mathematician Could Learn from Haskell"\;) \;\n \;\ nSPEAKER: \;\nLee Pike\, R&\;D Engineering\, Galois\, Inc. \;\n \;\nDATE: \;\nTuesday\, September 9th. 10.30am \;\n \;\nLOC ATION: \;\nGalois\, Inc. \;\n421 SW 6th Ave. Suite 300 \;\n( 3rd floor of the Commonwealth Building) \;\nPortland\, Oregon \;\n \;\nABSTRACT: \;\n \;\nTo the typical engineer or evaluator\, mathematics can be scary\, logic can be scarier\, and really long specif ications can simply be overwhelming. This talk is about the problem of t he visual presentation of formal specifications clearly and concisely. W e take as our initial inspiration Leslie Lamport's brief paper\, "\; How to Write a Long Formula"\; and "\;How to Write a Proof"\ ; in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification. \;\ n \;\nI will describe the problem and present one particular solution \, as implemented in a simple pretty-printer I've written (in Haskell)\, that uses indentation and labels to more easily visually parse long for mulas. Ultimately\, I propose a "\;HOL Normal Form"\; for presen ting specifications\, much like BNF is used for presenting language defi nitions. \;\n \;\nBIOGRAPHICAL DETAILS: \;\n \;\nhttp://galo is.com/company/people/lee_pike/ \;\n \;\nABOUT THE GALOIS TECH TAL KS. \;\n \;\nGalois (http://galois.com) has been holding weekly te chnical seminars for several years on topics from functional programming \, formal methods\, compiler and language design\, to cryptography\, and operating system construction\, with talks by many figures from the pro gramming language and formal methods communities. \;\n \;\nThe tal ks are open and free. If you're planning to attend\, dropping a note to is appreciated\, but not required. If you're interested in giving a tal k\, we're always looking for new speakers. \;\n\n\nTags: galois\, ha skell\, pdxfunc\, functional programming\n\nImported from: http://calaga tor.org/events/1250455680 SUMMARY:Galois Tech Talk: Pretty-Printing a Really Long Formula (or\, "Wh at a Mathematician Could Learn from Haskell") LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080915T100753Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080915T150000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080915T130000 DTSTAMP;VALUE=DATE-TIME:20080915T100753Z LAST-MODIFIED;VALUE=DATE-TIME:20210103T011025Z UID:http://calagator.org/events/1250455736 DESCRIPTION:Title: Left-fold enumerators \;\n Towards a safe\, expressive and efficient I/O interface for Haskell \;\n \ ;\nSpeaker: Johan Tibell \;\n Software Engineer \;\n Google \;\n \;\nDate: Monday\, September 15th.&# 13\;\n 1pm \;\n \;\nLocation: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \;\n (3rd floor of the Commonwealth Building) \;\n Portland\, Oregon \;\n \;\nAbstract: \;\n \;\n I will describe a programming style for I/O operations that is based on left-fold enumerators. This style of pr ogramming is more expressive than imperative style I/O represented by th e Unix functions read and write\, and safer than lazy I/O using streams. Left-fold enumerators offers both high-performance using block based I/ O and safety in terms of error handling and resource usage. I will demon strate Hyena\, a web server prototype written in Haskell\, as an example of left-fold enumerator style of programming. \;\n \;\n This t alk is intended as a starting point for further discussions on what woul d be a good interface for I/O rather than a presentation of finished res earch. \;\n \;\nAbout the Galois Tech Talks. \;\n \;\n Ga lois (http://galois.com) has been holding weekly technical seminars for several years on topics from functional programming\, formal methods\, c ompiler and language design\, to cryptography\, and operating system con struction\, with talks by many figures from the programming language and formal methods communities. \;\n \;\n The talks are open and f ree. If you're planning to attend\, dropping a note to is appreciated\, but not required. If you're interested in giving a talk\, we're always looking for new speakers. \;\n \;\n \;\nCrazybulk Avis \n\nTags : galois\, technology\, functional programming\, pdxfunc\n\nImported fro m: http://calagator.org/events/1250455736 SUMMARY:Galois Tech Talks: Left-fold enumerators -- Towards a safe\, expr essive and efficient I/O interface for Haskell LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080915T100544Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080916T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080916T103000 DTSTAMP;VALUE=DATE-TIME:20080915T100544Z LAST-MODIFIED;VALUE=DATE-TIME:20080915T100544Z UID:http://calagator.org/events/1250455735 DESCRIPTION:Title: Theorem Proving for Verification \;\n \;\nS peaker: John Harrison \;\n Principal Engineer \;\n Intel \;\n \;\nDate: Tuesday\, September 16th. \;\n 10.30am \;\n \;\nLocation: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \;\n (3rd floor of t he Commonwealth Building) \;\n Portland\, Oregon \;\n&# 13\;\nAbstract: \;\n \;\n The theorem proving approach to verif ication involves modelling a system in a rich formalism such as higher-o rder logic or set theory\, then performing a human-driven interactive co rrectness proof using a proof assistant. In a striking contrast\, techni ques like model checking\, by limiting the user to a less expressive for malism (propositional logic\, CTL etc.)\, can offer completely automated decision methods\, making them substantially easier to use and often mo re productive. \;\n \;\n With this in mind\, why should one be interested in the theorem proving approach? In this tutorial I will expl ain some of the advantages of theorem proving\, showing situations where the generality of theorem proving is beneficial\, allowing us to tackle domains that are beyond the scope of automated methods or providing oth er important advantages. I will talk about the state of the art in theor em proving systems and and give a little demonstration to give an impres sion of what it's like to work with such a system. \;\n \;\nBiogra phical details: \;\n \;\n John Harrison has worked in formal ve rification and automated theorem proving since 1990\, when he joined Mik e Gordon's "\;Hardware Verification Group"\; (HVG) at the Univer sity of Cambridge Computer Laboratory. As well as working on the develop ment of the HOL theorem prover\, he developed a particular interest in t he formalization of real analysis and its application to formal verifica tion of floating-point hardware. His PhD in this area\, "\;Theorem P roving with the Real Numbers"\;\, written under Mike Gordon's superv ision\, won a UK Distinguished Dissertation award and was published as a book. He also redesigned HOL from scratch\, resulting in an alternative version called HOL Light. After completing his PhD research in 1995\, J ohn Harrison spent a very enjoyable year at Abo Akademi University and T urku Centre for Computer Science (TUCS) in Turku\, Finland\, where he wa s a member of Ralph Back's Programming Methods Research Group. Among oth er activities\, he championed the "\;declarative"\; proofs of th e Mizar system and showed how these could be integrated into other theor em-provers\, work subsequently taken up in DECLARE\, Isar and other syst ems. \;\n \;\n John Harrison then returned to Cambridge and wor ked on a formal model of floating-point arithmetic and its application t o the verification of some realistic algorithms for transcendental funct ions. This work attracted the attention of Intel\, and in 1998 John Harr ison joined the company as a Senior Software Engineer (now Principal Eng ineer) specializing in the design and formal verification of mathematica l algorithms. He has formally verified and in many cases designed or red esigned numerous algorithms for mathematical functions including divisio n\, square root and transcendental functions. \;\n \;\n In his limited spare time over the past 10 years\, John Harrison has been worki ng on a book giving a comprehensive introduction to automated theorem pr oving. (http://www.cambridge.org/9780521899574) \;\n \;\nAbout th e Galois Tech Talks. \;\n \;\n Galois (http://galois.com) has b een holding weekly technical seminars for several years on topics from f unctional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system construction\, with talks by many figures from the programming language and formal methods communities.&# 13\;\n \;\n The talks are open and free. If you're planning to att end\, dropping a note to is appreciated\, but not required. If you're i nterested in giving a talk\, we're always looking for new speakers. \ ;\n\n\nTags: galois\, technology\, functional programming\, pdxfunc\n\nI mported from: http://calagator.org/events/1250455735 SUMMARY:Galois Tech Talk: Theorem Proving for Verification LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20080915T015716Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080918T180000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20080918T160000 DTSTAMP;VALUE=DATE-TIME:20080915T015716Z LAST-MODIFIED;VALUE=DATE-TIME:20080915T020057Z UID:http://calagator.org/events/1250455727 DESCRIPTION:We're having an Open House to celebrate our new office space in downtown Portland's historic Commonwealth Building. Located on SW 6th Avenue between Stark and Washington streets\, we're easily accessible v ia MAX or TriMet buses. We're up on the third floor. \;\nParking will also be available in the Alder Street Star Park parking garage located at 615 SW Alder\, just one block from our building\; validation will be provided at the event. \;\nRSVP: Anne Marie @ ph. 503.626.6616\, x153 or email anne at galois.com\n\nImported from: http://calagator.org/even ts/1250455727 SUMMARY:Galois Open House LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20081001T193211Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081002T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081002T103000 DTSTAMP;VALUE=DATE-TIME:20081001T193211Z LAST-MODIFIED;VALUE=DATE-TIME:20081001T193211Z UID:http://calagator.org/events/1250455788 DESCRIPTION:Title: Bluespec: Advanced Modeling\, Design and Verifica tion using High-Level Synthesis \;\nSpeaker: Rishiyur Nikhil CTO\, Bluespec\, Inc. \;\nDate: Thursday\, October 2nd. 10.30am \ ;\nLocation: Galois\, Inc.\, 421 SW 6th Ave. Suite 300\, (3rd floor of the Commonwealth Building) \;\n \;\n \;\nABSTRACT: \;\n \;\nOver the past few years\, several projects in major companies have b een adopting BSV (Bluespec SystemVerilog) as their next-generation tool of choice for IP design\, modeling (for both architecture exploration an d early software development)\, and verification enviroments. \;\n 3\;\nThe reason for choosing BSV is its unique combination of: \;\n&# 13\;\n(1) excellent computation model for expressing complex concurrency and communication\, based on atomic transactions and atomic transaction al inter-module methods \;\n \;\n(2) very high level of abstractio n and parameterization (principally inspired by Haskell) \;\n \;\n (3) full synthesizability\, enabling execution on FPGAs\, obtaining bett er performance (3 to 4 orders of magnitude) and scalability than softwar e simulation at comparable levels of detail. \;\n \;\nIn this pres entation\, I will provide a brief technical overview of BSV (points 1-3 above)\, and describe several customer projects using BSV. I will also briefly contrast BSV with other approaches to High Level Synthesis (part icularly those based on C/C++/SystemC). \;\n \;\n \;\nBIOGRAPHY : \;\n \;\nRishiyur S. Nikhil is co-founder and CTO of Bluespec\, Inc.\, which develops tools that dramatically improve correctness\, prod uctivity\, reuse and maintainability in the design\, modeling and verifi cation of digital designs (ASICs and FPGAs). The core technologies cons ist of a language\, BSV (Bluespec SystemVerilog)\, which enables very ab stract source descriptions based on scalable atomic transactions and ext reme parameterization\, and tools for high-quality synthesis of BSV into RTL. Earlier\, from 2000 to 2003\, he led a team inside Sandburst Corp. (later acquired by Broadcom) developing Bluespec technology and contrib uting to 10Gb/s enterprise network chip models\, designs and design tool s. \;\n \;\nFrom 1991 to 2000 he was at Cambridge Research Laborat ory (DEC/Compaq)\, including one and a half years as Acting Director. F rom 1984 to 1991 he was a professor of Computer Science and Engineering at MIT. He has led research teams\, published widely\, and holds severa l patents in functional programming\, dataflow and multithreaded archite ctures\, parallel processing\, compiling\, and EDA. He is a member of A CM and IFIP WG 2.8 on Functional Programming\, and a Senior Member of IE EE. He received his Ph.D. and M.S.E.E. in Computer and Information Scie nces from the Univ. of Pennsylvania\, and his B.Tech in EE from IIT Kanp ur. \;\n \;\n \;\nABOUT THE GALOIS TECH TALKS: \;\n \;\nG alois (http://galois.com) has been holding weekly technical seminars for several years on topics from functional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system co nstruction\, with talks by many figures from the programming language an d formal methods communities. \;\n \;\nThe talks are open and free . If you're planning to attend\, dropping a note to is appreciated\, bu t not required. If you're interested in giving a talk\, we're always loo king for new speakers.\n\nTags: galois\, technology\, functional program ming\, pdxfunc\, asic\, fpga\n\nImported from: http://calagator.org/even ts/1250455788 URL:http://galois.com SUMMARY:Galois Tech: Advanced Modeling\, Design and Verification using Hi gh-Level Synthesis LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20081006T223717Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081007T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081007T103000 DTSTAMP;VALUE=DATE-TIME:20081006T223717Z LAST-MODIFIED;VALUE=DATE-TIME:20081006T223717Z UID:http://calagator.org/events/1250455803 DESCRIPTION:Duncan Coutts\, from Well-Typed (http://well-typed.com)\, wil l be giving a tech talk tomorrow about the technical direction of Cabal\ , Haskell package infrastructure\, and the problems of managing very lar ge amounts of Haskell \;\ncode. \;\n \;\n... \;\n \;\nTIT LE: \;\nThe Future of Cabal -- "\;A language for build systems&qu ot\; and "\;Constraint solving problems in package deployment"\; \;\n \;\nSPEAKER: \;\nDuncan Coutts\, Well-Typed\, LLP \;\n \;\nDATE: \;\nTuesday\, Oct 7\, 2008 \;\n10.30am \;\n \; \nLOCATION: \;\nGalois\, Inc. \;\n421 SW 6th Ave. Suite 300 \;\ n(3rd floor of the Commonwealth Building) \;\nPortland\, Oregon \; \n \;\nABSTRACT: \;\n \;\nThis will be an informal talk and dis cussion on two topics: \;\n \;\n1. A language for build systems 3\;\n \;\nBuild systems are easy to start but hard to get right. We'l l take the view of a language designer and look at where our current too ls fall down in terms of safety/correctness and expressiveness. \;\n& #13\;\nWe'll then consider some very early ideas about what a build syst em language should look like and what properties it should have. Current ly this takes the form of a design for a build DSL embedded in Haskell.& #13\;\n \;\n2. Constraint solving problems in package deployment \ ;\n \;\nWe are all familiar\, at least peripherally\, with package sy stems. Every Linux distribution has a notion of packages and most have h igh level tools to automate the installation of packages and all their d ependencies. What is not immediately obvious is that the problem of reso lving a consistent set of dependencies is hard\, indeed it is NP-complet e. It is possible to encode 3-SAT or Sudoku as a query on a specially cr afted package repository. \;\n \;\nWe will look at this problem in a bit more detail and ask if the right approach might be to apply our k nowledge about constraint solving rather than the current ad-hoc solvers that most real systems use. My hope is to provoke a discussion about th e problem. \;\n \;\nWe can concentrate on one topic or the other d epending on peoples interest. \;\n \;\n \;\nABOUT THE GALOIS TE CH TALKS: \;\n \;\nGalois (http://galois.com) has been holding wee kly technical seminars for several years on topics from functional progr amming\, formal methods\, compiler and language design\, to cryptography \, and operating system construction\, with talks by many figures from t he programming language and formal methods communities. \;\n \;\nT he talks are open and free. If you're planning to attend\, dropping a no te to is appreciated\, but not required. If you're interested in giving a talk\, we're always looking for new speakers.\n\nTags: galois\, haske ll\, pdxfunc\, functional programming\n\nImported from: http://calagator .org/events/1250455803 URL:http://www.galois.com/ SUMMARY:Galois Tech Talk: The Future of Cabal (Haskell package management ) LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20081010T172812Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081014T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081014T103000 DTSTAMP;VALUE=DATE-TIME:20081010T172812Z LAST-MODIFIED;VALUE=DATE-TIME:20081010T172812Z UID:http://calagator.org/events/1250455813 DESCRIPTION:Next week's tech talk\, a special treat\, with Jason Dagit (a ka. lispy on \;\n#haskell) dropping by to talk about using GADTs to c lean up darcs' patch \;\ntheory implementation. \;\n \;\n------ ------------------------------------------------------------------ \; \n \;\nTITLE: \;\nType Correct Changes \;\nA Safe Approach to V ersion Control Implementation \;\n \;\nspeaker: \;\nJason Dagit \;\n \;\nLOCATION: \;\nGalois\, Inc. \;\n421 SW 6th Ave. Su ite 300 \;\n(3rd floor of the Commonwealth Building) \;\nPortland\ , Oregon \;\n \;\nABSTRACT: \;\n \;\nThis will be a talk abo ut Darcs and type safe manipulations of changes: \;\n \;\nDarcs is based on a data model\, known as Patch Theory\, that sets it apart from other version control systems. The power of this data model is that it allows Darcs to manage significant complexity with a relatively straigh tforward user interface. \;\n \;\nWe show that Generalized Algebra ic Data Types (GADTs) can be used to express several fundamental invaria nts and properties derived from Patch Theory. This gives our compiler\, GHC\, a way to statically enforce our adherence to the essential rules of our data model. \;\n \;\nFinally\, we examine how these techniq ues can improve the quality of the darcs codebase in practice. \;\n&# 13\;\nPRESENTER: \;\n \;\nJason Dagit graduated from Oregon State University with B.S. degrees in Computer Science and Mathematics. He is currently employed at PTV America while completing his Masters degree a t Oregon State under co-advisors Dr. David Roundy and Dr. Martin Erwig. During his time in graduate school he has studied both usability and pr ogramming languages. He participated in the 2007 Google Summer of Code where he worked under Dr. Roundy to improve Darcs conflict handling. \;\n \;\nABOUT THE GALOIS TECH TALKS: \;\n \;\nGalois (http://g alois.com) has been holding weekly technical seminars for several years on topics from functional programming\, formal methods\, compiler and la nguage design\, to cryptography\, and operating system construction\, wi th talks by many figures from the programming language and formal method s communities. \;\n \;\nThe talks are open and free. If you're pla nning to attend\, dropping a note to is appreciated\, but not required. If you're interested in giving a talk\, we're always looking for new sp eakers.\n\nTags: haskell\, galois\, pdxfunc\, functional programming\n\n Imported from: http://calagator.org/events/1250455813 URL:http://www.galois.com/ SUMMARY:Galois Tech Talk: Type Correct Changes\, A Safe Approach to Versi on Control Implementation LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20081027T212229Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081030T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20081030T103000 DTSTAMP;VALUE=DATE-TIME:20081027T212229Z LAST-MODIFIED;VALUE=DATE-TIME:20180831T072059Z UID:http://calagator.org/events/1250455994 DESCRIPTION:Factor is a programming language which has been in developmen t for a little over 5 years. Factor is influenced by Forth\, Lisp\, Smal ltalk. Factor takes the best ideas from Forth — simplicity\, short\, suc cint\, code\, emphasis on interactive testing\, and meta-programming. Fa ctor also brings modern high-level language features such as garbage col lection\, object orientation and functional programming familiar to user s of languages such as Lisp\, Smalltalk and Python. Finally\, recognizin g that no programming language is an island\, Factor is portable\, ships with a full-featured standard library\, deploys stand-alone binaries\, and interoperates with C and Objective-C. \;\n \;\nIn this talk\, I will give the rationale for Factor’s creation\, present an overview of the language\, and show how Factor can be used to solve real-world prob lems with a minimum of fuss. At the same time\, I will emphasize Factor’ s extensible syntax\, meta-programming and reflection capabilities\, and show that these features\, which are unheard of in the world of mainstr eam programming languages\, make programs easier to write\, more robust\ , and fun. \;\n \;\nBiography: \;\n Slava was born in the f ormer USSR and emigrated to New Zealand at the age of 7. He moved to Ott awa\, Canada when he was 18 to study for a Bachelors and Masters degree in Mathematics. He now resides in Minneapolis\, Minnesota. An early ado pter of Java\, Slava wrote the popular jEdit text editor\, then went on to design and implement the Factor programming language. At his day job he hacks on web apps\, optimizing compilers\, garbage collectors\, and e verything in between \;\n. \;\n Galois has been holding weekly t echnical seminars for several years on topics from functional programmin g\, formal methods\, compiler and language design\, to cryptography\, an d operating system construction\, with talks by many figures from the pr ogramming language and formal methods communities. \;\n \;\nThe ta lks are open and free. If you're planning to attend\, dropping a note to is appreciated\, but not required. If you're interested in giving a t alk\, we're always looking for new speakers. \n\nTags: functional progra mming\, galois\, lecture\, factor\, experimental language\n\nImported fr om: http://calagator.org/events/1250455994 URL:http://www.galois.com/blog/2008/10/24/factor-an-extensible-interactiv e-language/ SUMMARY:Galois Tech Talk: Slava Pestov on the Factor programming language LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090113T000344Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090113T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090113T103000 DTSTAMP;VALUE=DATE-TIME:20090113T000344Z LAST-MODIFIED;VALUE=DATE-TIME:20090113T000344Z UID:http://calagator.org/events/1250456454 DESCRIPTION:PRESENTATION \;\n \;\nTitle: OpenTheory: Package Manage ment for Higher Order Logic Theories \;\n \;\nSpeaker: Joe Hurd\, Galois\, Inc. \;\n \;\nAbstract: \;\n \;\nInteractive theore m has grown beyond toy examples in mathematics and program verification\ , as demonstrated by recent successes such as the Gonthier's formal proo f of the four colour theorem and Leroy's verified compiler from a realis tic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques\, th ere is now a need for theory engineering techniques to support these maj or verification efforts. \;\n \;\nIn this talk I will present the OpenTheory project\, which has defined a simple 'article' format to repr esent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover\, compressed by a stand alone tool\, stored and read by a different theorem prover. Articles nat urally support theory interpretations\, which leads to more efficient de velopments of standard theories\, and also provides one approach to hand ling difficult constructs such as monads without extending the underlyin g logic. Finally\, the grand vision of the OpenTheory article repository is painted\, with fully automatic installation and dependency resolutio n. \;\n \;\nABOUT THE GALOIS TECH TALKS: \;\n \;\nGalois (ht tp://galois.com) has been holding weekly technical seminars for several years on topics from functional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system constructio n\, with talks by many figures from the programming language and formal methods communities. \;\n \;\nThe talks are open and free. If you' re planning to attend\, dropping a note to donsATgaloisDOTcom is appreci ated\, but not required. If you're interested in giving a talk\, we're always looking for new speakers. \;\n\n\nTags: galois\n\nImported fr om: http://calagator.org/events/1250456454 URL:http://www.galois.com/blog/2009/01/08/tech-talk-opentheory-package-ma nagement-for-higher-order-logic-theories/ SUMMARY:Galois Tech Talk: OpenTheory\, Package Management for Higher Orde r Logic Theories LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090120T051104Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090120T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090120T103000 DTSTAMP;VALUE=DATE-TIME:20090120T051104Z LAST-MODIFIED;VALUE=DATE-TIME:20090120T051104Z UID:http://calagator.org/events/1250456553 DESCRIPTION:The next Galois Tech Talk\, #2 for 2009\, will be Isaac Potoc zny-Jones (aka SyntaxNinja) on developing for the Android G1 phone. \ ;\n \;\n The Android G1 is a TMobile phone whose operating system\ , Android is based on Linux and was developed by Google. It’s a very ope n smart-phone platform that rivals the iPhone. \;\n \;\n While I’m no expert in Android or mobile platform development\, I will discuss my experiences in Android development and demonstrate the toolchain use d to develop software for the Android. I’ll outline the basic features o f the platform\, with a focus on the factors that make its openness so p owerful: \;\n \;\n * the inter-process communications mechanism whereby applications can advertise the services they offer and other ap plications can take advantage of those services\, \;\n \;\n * T he open-source Java\, Eclipse\, and Linux-based toolchain\, \;\n \ ;\n * the OpenIntents project. \;\n \;\n This will be an inf ormal demonstration and discussion. \;\n \;\n A group of us in collaboration between the Android Password Safe project and the Openinte nts project have implemented a cryptography service and a keystore servi ce which other Android applications can use to keep data and passwords s afe\, in a way that’s convenient for the end user. \;\n \;\n Ou r system allows a single password\, and periodic single sign-on so that all applications can encrypt\, decrypt\, and store keys using the same m aster password that the user enters once. \;\n \;\n * Date: Tu esday\, January 20\, 2008 \;\n * Time: 10:30am - 11:30am \;\n * Location: Galois\, Inc. \;\n 421 SW 6th Ave. Suite 300 \; \n (3rd floor of the Commonwealth Building) \;\n Portland\, OR 97204 \;\n \;\nGalois has been holding weekly technical semina rs for several years on topics from functional programming\, formal meth ods\, compiler and language design\, to cryptography\, and operating sys tem construction\, with talks by many figures from the programming langu age and formal methods communities. The talks are open and free. \;\n \n\nTags: galois\, android\n\nImported from: http://calagator.org/events /1250456553 URL:http://www.galois.com/blog/2009/01/19/tech-talk-android-g1-experience s-with-an-open-mobile-platform/ SUMMARY:Galois Tech Talk: Android G1: Experiences with an open mobile pla tform LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090703T083359Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090707T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090707T103000 DTSTAMP;VALUE=DATE-TIME:20090703T083359Z LAST-MODIFIED;VALUE=DATE-TIME:20090703T083359Z UID:http://calagator.org/events/1250457382 DESCRIPTION:Abstract: This talk describes a radically different architect ure for computing called Fleet. Fleet accepts the limitations to computi ng imposed by physics: moving data around inside a computer costs more e nergy\, more delay\, and more chip area than the arithmetic and logical operations ordinarily called “computing.” Fleet puts the programmer firm ly in charge of the most costly resource\, communication\, instead of in charge of the arithmetic and logical resources that are now almost free . Fleet treats arithmetic and logical operations as side effects of wher e the programmer sends data. \;\n \;\nFleet achieves high performa nce through fine grain concurrency. Everything Fleet does is concurrent at the lowest level\; programmers who wish sequentiality must program it explicitly. Fleet presents a stark contrast to today’s multi-core machi nes in which programmers seek concurrency in an inherently sequential en vironment. \;\n \;\nThe Fleet architecture uses a uniform switch f abric to simplify chip design. A few thousand identical copies of a prog rammable interface connect a thousand or so repetitions of basic arithme tic\, logical\, input-output\, and storage units to the switch fabric. T he uniform switch fabric and its identical programmable interfaces repla ce many of the hard parts of designing the computing elements themselves . \;\n \;\nBoth software and FPGA simulators of a Fleet system are available at UC Berkeley. Berkeley students have written a variety of F leet programs\; their work helped to define what the programmable interf ace between computing and communication must do. A simple compiler now p roduces the programs required at source and destination to provide flow- controlled communication. We expect work on a higher-level language to a ppear soon as a PhD dissertation. \;\n \;\nA recent 90 nanometer T SMC test chip\, called Infinity\, demonstrated switch fabric performance at about 4 GHz. A new test chip\, called Marina\, has just gone out for fabrication. Marina will test the programmable interface\, and if succe ssful\, will give us confidence to build a complete Fleet. We seek parti cipation from sponsors\, programmers\, and designers of basic computatio n elements. \;\n \;\nBio: Ivan Sutherland is a Visiting Scientist at Portland State University where he and Marly Roncken have recently es tablished the “Asynchronous Research Center” (ARC). The ARC occupies bot h physical and intellectual space half way between the Computer Science (CS) and Electrical and Computer Engineering (ECE) departments at the un iversity. The ARC seeks to free designers from the tyranny of the clock by developing better tools and teaching methods for design of self-timed systems. Prior to moving to Portland\, Ivan spent 25 years as a Fellow and Vice President at Sun Microsystems. A graduate of Carnegie Tech\, Iv an got his PhD at MIT in 1963 and has taught at Harvard\, University of Utah\, and Caltech. \;\n \;\nDr. Sutherland received the 1998 Turi ng Award\, for his pioneering work in the field of computer graphics.\n\ nImported from: http://calagator.org/events/1250457382 URL:http://www.galois.com/blog/2009/06/30/fleet/ SUMMARY:Galois Talk: The Fleet Architecture by Ivar Sutherland LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090724T154624Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090728T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090728T103000 DTSTAMP;VALUE=DATE-TIME:20090724T154624Z LAST-MODIFIED;VALUE=DATE-TIME:20090724T154624Z UID:http://calagator.org/events/1250457471 DESCRIPTION:The July 28th Galois Tech Talk will be delivered by Joe Hurd\ , titled “Mathematics of Cryptography: A Guided Tour.” \;\n \;\n * Date: Tuesday\, July 28th\, 2009 \;\n * Time: 10:30am - 11:30a m \;\n * Location: Galois\, Inc. \;\n 421 SW 6th Ave. Suit e 300 \;\n (3rd floor of the Commonwealth Building) \;\n Portland\, OR 97204 \;\n \;\nAbstract: In this informal talk I’ll give a guided tour of the mathematics underlying cryptography. No prior knowledge will be assumed: the goal of the talk is to demonstrate how s imple mathematical concepts from algebra and number theory are used to b uild a wide range of cryptographic algorithms\, from the familiar (encry ption) to the exotic (zero knowledge proofs). \;\n \;\nBio: Joe Hu rd is a Formal Methods Engineer at Galois\, Inc. He completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs\, and his work since has included: developing a package manage ment system for higher order logic theories\; applying automatic proof t echniques for first order logic\; and creating the world’s first formall y verified chess endgame database.\n\nImported from: http://calagator.or g/events/1250457471 URL: http://www.galois.com/blog/2009/07/22/cryptomath/ SUMMARY:Galois Talk: Mathematics of Cryptography: A Guided Tour LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090819T232300Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090825T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090825T103000 DTSTAMP;VALUE=DATE-TIME:20090819T232300Z LAST-MODIFIED;VALUE=DATE-TIME:20090819T232300Z UID:http://calagator.org/events/1250457585 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n * Date: Tuesday\, August 25th\, 2009 \;\n * Title: Programming th e Fleet \;\n * Speaker: Adam Megacz \;\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 blog post: http://www.galois.com/blog/2009/08/19/ programmingfleet/ \;\n \;\nAn RSVP is not required\; but feel free to drop a line to levent.erkok@galois.com if you've any questions or co mments. \;\n \;\nLevent Erkok\n\nTags: tech seminar\, fleet\, arch itecture\n\nImported from: http://calagator.org/events/1250457585 URL:http://www.galois.com/blog/2009/08/19/programmingfleet/ SUMMARY:Galois Talk: Programming the fleet LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090911T065240Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090918T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090918T103000 DTSTAMP;VALUE=DATE-TIME:20090911T065240Z LAST-MODIFIED;VALUE=DATE-TIME:20090911T065240Z UID:http://calagator.org/events/1250457665 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n[Note the Friday date\, instead of the usual Tuesday slot!] \;\n&# 13\;\n * Date: Friday\, September 18th\, 2009 \;\n * Title: Building Systems That Enforce Measurable Security Goals \;\n * Speaker: Trent Jaeger \;\n * Time: 10:30am - 11:30am \;\n * Location: Galois\, In c. 421 SW 6th Ave. Suite 300\; Portland\, OR \;\n97204 \;\n \;\ nFor details (including an abstract and speaker bio)\, please see our 3\;\nblog post: http://www.galois.com/blog/2009/09/10/jaegermeasurablese curit/ \;\n \;\nAn RSVP is not required\; but feel free to drop a line to \;\nlevent.erkok@galois.com if you've any questions or commen ts. \;\n \;\nLevent Erkok\n\nTags: tech seminar\, galois\, securit y\n\nImported from: http://calagator.org/events/1250457665 URL:http://www.galois.com/blog/2009/09/10/jaegermeasurablesecurit/ SUMMARY:Building Systems That Enforce Measurable Security Goals LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:0 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20090930T044415Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091006T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091006T103000 DTSTAMP;VALUE=DATE-TIME:20090930T044415Z LAST-MODIFIED;VALUE=DATE-TIME:20091006T013224Z UID:http://calagator.org/events/1250457759 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n* Date: Tuesday\, October 6th\, 2009 \;\n* Title: Roll Your Own Te st Bed for Embedded Real-Time Protocols: A Haskell Experience \;\n* S peaker: Lee Pike \;\n* Time: 10:30am - 11:30am \;\n* Location: Gal ois\, Inc. 421 SW 6th Ave. Suite 300\; Portland\, OR 97204 \;\n \; \nFor details (including an abstract and speaker bio)\, please see our&# 13\;\nblog post: http://www.galois.com/blog/2009/09/29/pike-haskell0/ 3\;\n \;\nAbstract: We present by example a new application domain fo r functional languages: emulators for embedded real-time protocols. As a case-study\, we implement a simple emulator for the Biphase Mark Protoc ol\, a physical-layer network protocol in Haskell. The surprising result is that a pure functional language with no built-in notion of time is e xtremely well-suited for constructing such emulators. Furthermore\, we u se Haskell’s property-checker QuickCheck to automatically generate real- time parameters for simulation. We also describe a novel use of QuickChe ck as a probability calculator for reliability analysis. \;\n \;\n Bio: Lee Pike is a member of the technical staff at Galois. Previously\, he was a research scientist with the NASA Langley Formal Methods Group\ , primarily involved in the SPIDER project. His research interests inclu de applying formal methods to safety-critical and security-critical appl ications\, with a focus on industrial-scale endeavors. \;\n \;\nAn RSVP is not required\; but feel free to drop a line to \;\nlevent.er kok@galois.com if you've any questions or comments. \;\n \;\nLeven t Erkok\n\nTags: galois\, haskell\, tech seminar\, quickcheck\, real-tim e\, simulation\n\nImported from: http://calagator.org/events/1250457759 URL:http://www.galois.com/blog/2009/09/29/pike-haskell0/ SUMMARY:Galois Tech Talk: Roll Your Own Test Bed for Embedded Real-Time P rotocols: A Haskell Experience LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:3 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091006T184249Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091013T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091013T103000 DTSTAMP;VALUE=DATE-TIME:20091006T184249Z LAST-MODIFIED;VALUE=DATE-TIME:20091006T184249Z UID:http://calagator.org/events/1250457835 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n * Date: Tuesday\, October 13th\, 2009 \;\n * Title: Constructin g A Universal Domain for Reasoning About Haskell \;\nDatatypes \;\ n * Speaker: Brian Huffman \;\n * Time: 10:30am - 11:30am \;\n * Location: Galois\, Inc. 421 SW 6th Ave. Suite 300\; Portland\, OR \ ;\n97204 \;\n \;\nFor details (including an abstract and speaker b io)\, please see our \;\nblog post: http://www.galois.com/blog/2009/1 0/06/huffman-universal/ \;\n \;\nAn RSVP is not required\; but fee l free to drop a line to \;\nlevent.erkok@galois.com if you've any qu estions or comments. \;\n \;\nLevent Erkok \n\nTags: galois\, tech talk\, theorem proving\n\nImported from: http://calagator.org/events/12 50457835 URL:http://www.galois.com/blog/2009/10/06/huffman-universal/ SUMMARY:Galois Talk: Constructing a Universal Domain for reasoning about Haskell Datatypes LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091013T233842Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091020T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091020T103000 DTSTAMP;VALUE=DATE-TIME:20091013T233842Z LAST-MODIFIED;VALUE=DATE-TIME:20091013T233842Z UID:http://calagator.org/events/1250457859 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n* Date: Tuesday\, October 20th\, 2009 \;\n* Title: Writing Linux K ernel Modules with Haskell \;\n* Speaker: Thomas DuBuisson \;\n* T ime: 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/13/haskellkernelmodules/ \;\n \;\nAn RSVP is not required\; but feel free to drop a line to \;\nlevent.erkok@g alois.com if you've any questions or comments. \;\n \;\nLevent Erk ok\n\nTags: galois\, tech talk\, haskell\, linux kernel modules\n\nImpor ted from: http://calagator.org/events/1250457859 URL:http://www.galois.com/blog/2009/10/13/haskellkernelmodules/ SUMMARY:Galois Talk: Writing Linux Kernel Modules with Haskell LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 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:20091028T215944Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091103T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091103T103000 DTSTAMP;VALUE=DATE-TIME:20091028T215944Z LAST-MODIFIED;VALUE=DATE-TIME:20091028T215944Z UID:http://calagator.org/events/1250457935 DESCRIPTION:The next talk in the Galois Tech Seminar series: \;\n \ ;\n * Date: Tuesday\, November 3rd\, 2009 \;\n * Title: Testing Fir st-Order-Logic Axioms in AutoCert \;\n * Speaker: Ki Yung Ahn \;\ n * Time: 10:30am - 11:30am \;\n * Location: Galois\, Inc. 421 SW 6 th Ave. Suite 300\; Portland\, OR \;\n97204 \;\n \;\nFor detail s (including an abstract and speaker bio)\, please see our \;\nblog p ost: http://www.galois.com/blog/2009/10/28/ahn-autocert/ \;\n \;\n An RSVP is not required\; but feel free to drop a line to \;\nlevent. erkok@galois.com if you've any questions or comments. \;\n \;\nLev ent Erkok \n\nTags: galois\, haskell\, smt\, yices\, testing\, first-ord er-logic\, tech talk\n\nImported from: http://calagator.org/events/12504 57935 URL:http://www.galois.com/blog/2009/10/28/ahn-autocert/ SUMMARY: Galois Talk: Testing First-Order-Logic Axioms in AutoCert LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091104T203648Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091113T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091113T103000 DTSTAMP;VALUE=DATE-TIME:20091104T203648Z LAST-MODIFIED;VALUE=DATE-TIME:20091104T203648Z UID:http://calagator.org/events/1250457967 DESCRIPTION:[NB. This talk is on Friday\, instead of the usual Tuesday sl ot.] \;\n \;\nThe next talk in the Galois Tech Seminar series: \;\n \;\n * Date: Friday\, November 13th\, 2009 \;\n * Title: Hoar e-Logic – fiddly details and small print \;\n * Speaker: Rod Chapman& #13\;\n * Time: 10:30am - 11:30am \;\n * Location: Galois\, Inc. 421 SW 6th Ave. Suite 300\; Portland\, OR \;\n97204 \;\n \;\nFor de tails (including an abstract and speaker bio)\, please see our \;\nbl og post: http://www.galois.com/blog/2009/11/04/chapman-hoare/ \;\n 3\;\nAn RSVP is not required\; but feel free to drop a line to \;\nle vent.erkok@galois.com if you've any questions or comments. \;\n \; \nLevent Erkok\n\nTags: galois\, tech talk\, hoare logic\, praxis\, veri fication\n\nImported from: http://calagator.org/events/1250457967 URL:http://www.galois.com/blog/2009/11/04/chapman-hoare/ SUMMARY:Galois Talk: Hoare-Logic – fiddly details and small print LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091111T163333Z DTEND;VALUE=DATE:20091116 DTSTART;VALUE=DATE:20091114 DTSTAMP;VALUE=DATE-TIME:20091111T163333Z LAST-MODIFIED;VALUE=DATE-TIME:20091111T163333Z UID:http://calagator.org/events/1250457992 DESCRIPTION:This event runs from Saturday\, November 14\, 2009 at 9am thr ough Sunday\, November 15\, 2009 at 5pm.\n\nDescription:\nWho : Anybody who wants to hack on Darcs (or Camp\, Focal\, SO6\, etc) Beginners espe cially welcome! \;\n \;\nWhy : Darcs aims to have bi-annual hacki ng sprints so that we can get together on a regular basis\, hold design discussions\, hack up a storm and have a lot fun. \;\n \;\nWhat : We plan to put some finishing touches on Darcs-2.4. Darcs 2.4 is a prett y exciting release because we expect it to offer nice performance enhanc ements from Petr's Google \;\n \;\nSummer of Code Project\, and al so a nice new 'hunk splitting' feature. \;\n \;\nWe also intend to set aside at least one Darcs hacker for mentoring beginners\, so if you 're new to Haskell or to Darcs hacking\, here's a good chance to plunge in and start working on a real world project. \;\n \;\nHow: Add yourself to http://wiki.darcs.net/Sprints/2009-11\n\nTags: darcs\, haske ll\, programming\n\nImported from: http://calagator.org/events/125045799 2 URL:http://wiki.darcs.net/Sprints/2009-11 SUMMARY:Darcs Hacking Sprint LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091210T001647Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091215T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20091215T103000 DTSTAMP;VALUE=DATE-TIME:20091210T001647Z LAST-MODIFIED;VALUE=DATE-TIME:20091211T174224Z UID:http://calagator.org/events/1250458080 DESCRIPTION:The December 15th Galois Tech Talk will be delivered by John Launchbury. He will present Conal Elliott’s 2009 ICFP paper entitled B eautiful Differentiation for those of us who were not able to attend thi s wonderful talk in-person.\n\nTags: galois\, haskell\, functional progr amming\n\nImported from: http://calagator.org/events/1250458080 URL:http://www.galois.com/blog/2009/12/09/tech-talk-john-launchbury-prese nts-conal-elliots-beautiful-differentiation/ SUMMARY:Galois Tech Talk: Beautiful Differentiation LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:4 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20091231T014423Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100105T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100105T103000 DTSTAMP;VALUE=DATE-TIME:20091231T014423Z LAST-MODIFIED;VALUE=DATE-TIME:20091231T015006Z UID:http://calagator.org/events/1250458113 DESCRIPTION:The next Galois Tech Talk will be delivered by Amit Goel. Co me kick off 2010 with us! \;\n \;\nTitle: Ground Interpolation for Combined Theories \;\n \;\nAbstract: We give a method for modular generation of ground interpolants in modern SMT solvers supporting mult iple theories. Our method uses a novel algorithm to modify the proof tre e obtained from an unsatifiability run of the solver into a proof tree w ithout occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for con vex theories) on the search strategy of the solver. Consequently\, it is straightforward to implement and enables more efficient interpolating S MT solvers. In the presence of non-convex theories our method is incompl ete\, but still more general than previous methods. \;\n \;\n * Date: Tuesday\, 10:30am\, 05 Jan 2010 \;\n * Time: 10:30am – 11:3 0am \;\n * Location: Galois\, Inc. \;\n 421 SW 6th Ave. Su ite 300 \;\n (3rd floor of the Commonwealth Building) \;\n Portland\, OR 97204 \;\n \;\nBio: Amit Goel is a member of Inte l’s Strategic CAD Labs.\n\nImported from: http://calagator.org/events/12 50458113 URL:http://www.galois.com/blog/2009/12/30/tech-talk-ground-interpolation- for-combined-theories/ SUMMARY:Galois Tech Seminar LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:4 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100120T195950Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100129T143000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100129T133000 DTSTAMP;VALUE=DATE-TIME:20100120T195950Z LAST-MODIFIED;VALUE=DATE-TIME:20100120T200204Z UID:http://calagator.org/events/1250458206 DESCRIPTION:A Scalable I/O Manager for GHC \;\n \;\nPresented by Jo han Tibell. \;\n \;\nAbstract: The Glasgow Haskell Compiler suppor ts extraordinarily cheap threads. These are implemented using a two-leve l model\, with threads scheduled across a set of OS-level threads. Since the lightweight threads can’t afford to block when performing I/O opera tions\, when a Haskell program starts\, it runs an I/O manager thread wh ose job is to notify other threads when they can safely perform I/O. \;\n \;\nThe I/O manager manages its file descriptors using the selec t system call. While select performs well for a small number of file des criptors\, it doesn’t scale to a large number of concurrent clients\, ma king GHC less attractive for use in large-scale server development. \ ;\n \;\nThis talk will describe a new\, more scalable I/O manager tha t’s currently under development and that hopefully will replace the curr ent I/O manager in a future release of GHC. \;\n \;\nDetails: \ ;\nDate: January 29th\, 2010\, Friday \;\nTime: 1:30pm \;\nLocatio n: Galois Inc.\, 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwea lth building) \;\n \;\nBio: Johan Tibell is a Software Engineer at Google Inc. He received a M.S. in Software Engineering from the Chalmer s University of Technology\, Sweden\, in 2007.\n\nTags: haskell\, ghc\, concurrency\n\nImported from: http://calagator.org/events/1250458206 URL:http://www.galois.com/blog/2010/01/20/tech-talk-a-scalable-io-manager -for-ghc/ SUMMARY:Galois Tech Talk: A Scalable I/O Manager for GHC LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:4 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:20100211T190104Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100216T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100216T103000 DTSTAMP;VALUE=DATE-TIME:20100211T190104Z LAST-MODIFIED;VALUE=DATE-TIME:20100211T190104Z UID:http://calagator.org/events/1250458313 DESCRIPTION:The talk will be presented by Iavor Diatchki on Tuesday\, Feb ruary \;\n16th\, at 10:30am. \;\n \;\nAbstract: GF is a progr amming language for multilingual grammar \;\napplications. It may b e seen in a number of different ways: \;\n \;\n • as a special-pur pose language for grammars\, like YACC or Happy\, \;\nbut not restr icted to programming languages\; \;\n • as a functional language\, li ke Haskell or SML\, but specialized to \;\ngrammar writing\; \;\ n • as a logical framework\, like Agda or Coq\, but equipped with \ ;\nconcrete syntax in addition to logic\; \;\n • as a natural languag e processing framework\, like LKB\, or Regulus\, \;\nbut based on f unctional programming and type theory. \;\nThis talk is an introducti on to GF’s basic concepts by example. We \;\nwill look at how to de fine the meaning and syntax of a language\, \;\nperform simple tran slations\, define semantic properties\, and how to \;\nuse GF toget her with another language such as Haskell. \;\n \;\nBio: Iavor Dia tchki is a R&\;D Engineer at Galois\, Inc. with a Ph.D. \;\nfrom the Oregon Graduate Institute. \;\n \;\nDetails: \;\n \;\n • Date: February 16th\, 2010\, Tuesday \;\n • Time: 10:30am \;\n • Location: Galois Inc.\, 421 SW 6th Ave. Suite 300 (3rd floor of \;\nthe Commonwealth building)\n\nImported from: http://calagator.org/ev ents/1250458313 URL:http://www.galois.com/blog/2010/02/11/tech-talk-introduction-to-gf-th e-grammatical-framework/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100219T220945Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100223T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100223T103000 DTSTAMP;VALUE=DATE-TIME:20100219T220945Z LAST-MODIFIED;VALUE=DATE-TIME:20100219T220945Z UID:http://calagator.org/events/1250458335 DESCRIPTION:Galois has been holding weekly technical seminars for several years on topics from functional programming\, formal methods\, compiler and language design\, to cryptography\, and operating system constructi on\, with talks by many figures from the programming language and formal methods communities. The talks are open and free.\n\nImported from: htt p://calagator.org/events/1250458335 URL:http://www.galois.com/blog/2010/02/19/tech-talk-modern-benchmarking-i n-haskell/ SUMMARY:Galois Tech Talk: Modern Benchmarking in Haskell LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100311T003027Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100315T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100315T103000 DTSTAMP;VALUE=DATE-TIME:20100311T003027Z LAST-MODIFIED;VALUE=DATE-TIME:20100311T003027Z UID:http://calagator.org/events/1250458415 DESCRIPTION:Haskell is an excellent language for combining the power of f unctional programming with imperative constructs. This characteristic le d to the development of the Communicating Haskell Processes (CHP) librar ies\, which support imperative synchronous message-passing in Haskell. T he core 'chp' library provides basic message-passing\, concurrency and c hoice\, as well as integrated support for tracing. The 'chp-plus' librar y provides higher-level features such as process composition operators a nd behaviour combinators. This talk provides an introduction to the two libraries and the programming style they engender -- as well as a brief look at the formal semantics underlying the libraries.\n\nImported from: http://calagator.org/events/1250458415 URL:http://www.galois.com/blog/2010/03/10/tech-talk-an-introduction-to-co mmunicating-haskell-processes/ SUMMARY:Galois Tech Talk: An Introduction to Communicating Haskell Proces ses LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100320T234321Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100324T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100324T103000 DTSTAMP;VALUE=DATE-TIME:20100320T234321Z LAST-MODIFIED;VALUE=DATE-TIME:20100324T035202Z UID:http://calagator.org/events/1250458462 DESCRIPTION:Galois is pleased to host two tech talks on Wed.\, March 24.& #13\;\n \;\nVisualization and Diversity Information \;\n \;\nDe tails: \;\n \;\n * Presenter: Prof. Ron Metoyer \;\n * Da te: Wednesday\, March 24\, 2010 \;\n * Time: 10:30am \;\n \; \nAbstract: The term “diversity’’ is used in many ways in many domains. People are concerned about the diversity of their work force\, stock po rtfolios\, student body\, and forest insects\, just to name a few. In t his talk\, I will discuss a work-in-progress visualization technique spe cifically designed to communicate diversity information. I will present the design concerns\, resulting visualizations\, and a study design for evaluating the method. I will conclude with a discussion of a case-stu dy application to moth species data. \;\n \;\nBio: Ronald Metoyer is an Associate Professor in the School of Electrical Engineering and Co mputer Science at Oregon State University. He earned a Ph.D. from the G eorgia Institute of Technology where he worked in the Graphics\, Visuali zation and Usability Center with a focus on modeling and visualizing the motion of pedestrians in urban and architectural scenes. Dr. Metoyer c urrently co-directs the NVIDIA Graphics and Imaging Technologies Lab (GA IT) with his colleagues at OSU. His past research efforts have involved the investigation of techniques for manipulating motion capture data and for facilitating the creation of 3D content by end users with the goal of empowering domain experts to create compelling and interactive conten t for their domain specific needs. In 2002\, he received an NSF CAREER Award for his work in “Understanding the Complexities of Animated Conten t”. Dr. Metoyer’s most recent research interests fall under the domain of information visualization. \;\n \;\n--------------------------- --- \;\n \;\nTITLE: Scientific Data Visualization in a GPU World&# 13\;\n \;\nDetails: \;\n \;\n * Presenter: Prof. Mike Bailey \;\n * Date: Wednesday\, March 24\, 2010 \;\n * Time: 11:00 am \;\n \;\nAbstract: One of the fun aspects of scientific data vi sualization is that there are no rules — anything that adds insight to t he data display is fair game. Add that to the fun of custom-programming the GPU\, and you’ve really got something! \;\n \;\nThis talk wil l discuss some of the uses of custom GPU programming to create better an d more interactive visualization displays. We will look at techniques i n the realm of scalar visualization\, vector visualization\, volume visu alization\, and terrain mapping. \;\n \;\nBio: Mike Bailey is a Pr ofessor in Computer Science at Oregon State University. He specializes i n scientific visualization\, 3D interactive computer graphics\, GPU prog ramming\, stereographics\, and computer aided geometric design.\n\nImpor ted from: http://calagator.org/events/1250458462 URL:http://www.galois.com/blog/2010/03/20/tech-talk-three-talks-one-week/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100320T234421Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100401T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100401T103000 DTSTAMP;VALUE=DATE-TIME:20100320T234421Z LAST-MODIFIED;VALUE=DATE-TIME:20100324T035334Z UID:http://calagator.org/events/1250458463 DESCRIPTION:********* \;\n** NOTICE: This talk has been postponed unti l April 1 at 10:30am. \;\n********* \;\n \;\nBuilding Refactori ng Tools for Functional Languages \;\n \;\nDetails: \;\n \;\ n * Presenter: Prof. Simon Thompson \;\n * Date: Thursday\, Apr il 1\, 2010 \;\n * Time: 10:30am \;\n \;\nAbstract: Refactor ing is the process of changing the design of a program without changing what it does. Typical refactorings\, such as function extraction and gen eralisation\, are intended to make a program more amenable to extension\ , more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code (rather than wit hin the bowels of a compiler)\, and in having an effect across a code ba se. Because of this\, there is a need to give (semi-)automated support t o the process. This talk will reflect on our experience of building too ls to refactor functional programs written in Haskell (HaRe?) and Erlan g (Wrangler). In doing this we will address system design\, the pragmati cs of system take-up\, as well as contrasting the style of refactoring a nd tooling for Haskell and Erlang. \;\n \;\nBio: Simon Thompson is a Professor of Logic and Computation at the University of Kent.\n\nImpo rted from: http://calagator.org/events/1250458463 URL:http://www.galois.com/blog/2010/03/20/tech-talk-three-talks-one-week/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100422T155706Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100427T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100427T103000 DTSTAMP;VALUE=DATE-TIME:20100422T155706Z LAST-MODIFIED;VALUE=DATE-TIME:20100422T155706Z UID:http://calagator.org/events/1250458589 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\nThe talk will be held at \;\n \;\nGalois Inc. \;\n421 SW 6th Ave. S uite 300\, Portland\, OR\, USA \;\n(3rd floor of the Commonwealth bui lding) \;\n \;\nVisualizing Information Flow through C Programs 3\;\n \;\nDetails: \;\n \;\n * Presenter: Joe Hurd \;\n * Date: Tuesday April 27\, 2010 \;\n * Time: 10:30am \;\n \;\nAbstract: The aim of the Automated Security Analysis project is to d etermine whether the information flows in a realistically-sized C codeba se can be automatically deduced and communicated in an understandable wa y to someone unfamiliar with the code. To test this\, a new information flow static analysis and visualization technique were developed\, and im plemented in a research prototype tool. This talk will present the novel features of the static analysis and demonstrate how the results are sho wn in the visualization tool: information flow between program storage l ocations is decomposed into two compositional properties\, which can be computed using sound abstract interpretation techniques. For each deduce d information flow\, the static analysis keeps track of a set of source code locations which demonstrate the information flow\, and this is used by the visualization component to communicate the information flow to a user browsing the source code. \;\n \;\nBio: Joe Hurd\, Ph.D. is a Formal Methods Engineer at Galois\, Inc. For the past ten years Dr. Hu rd has been applying theorem proving techniques to formally verify the c orrectness of complex software\, including probabilistic programs\, elli ptic curve cryptography and game tree analysis algorithms. He is also th e developer of Metis\, an automatic theorem prover for first order logic \, and coordinates the OpenTheory project\, a package management system for higher order logic theories. Dr. Hurd is an active member of the the orem proving research community\, having organized conferences in 2005 a nd 2008\, given invited talks\, and regularly appears on program committ ees and reviews papers for conferences and journals. Prior to joining Ga lois in 2007\, Dr. Hurd was a research fellow at Magdalen College\, Univ ersity of Oxford. He studied at the University of Cambridge\, receiving a Masters level degree in Mathematics in 1997\, and a Ph.D. in Computer Science in 2002.\n\nImported from: http://calagator.org/events/125045858 9 URL:http://www.galois.com/blog/2010/04/22/tech-talk-visualizing-informati on-flow-through-c-programs/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100430T190116Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100503T163000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100503T153000 DTSTAMP;VALUE=DATE-TIME:20100430T190116Z LAST-MODIFIED;VALUE=DATE-TIME:20100503T055219Z UID:http://calagator.org/events/1250458627 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\nThe talk will be held at \;\n \;\nGalois Inc. \;\n421 SW 6th Ave. S uite 300\, Portland\, OR\, USA \;\n(3rd floor of the Commonwealth bui lding) \;\nTyping Directories \;\n \;\nDetails: \;\n \;\n * Presenter: Kathleen Fisher\, AT&\;T Labs \;\n * Date: Mon day May 03\, 2010 \;\n * Time: 3:30pm \;\n \;\nTitle: Typing Directories \;\n \;\nAbstract: PADS describes the contents of ind ividual ad hoc data files\, but has no provisions for describing collect ions of files\, i.e.\, directories. In this talk\, I explore examples wh ere having a declarative description of directories as well as files wou ld be useful\, including websites\, source code trees\, source code cont rol systems\, operating systems\, and scientific data sets. As part of t his exploration\, I identify essential features of a directory descripti on language and useful tools that might be produced from such a descript ion. I end with a series of questions about how such a language might mo st easily be implemented in the context of Haskell. \;\n \;\nThis is joint work with David Walker and Kenny Zhu. \;\n \;\nBio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher i s a Principal Member of the Technical Staff at AT&\;T Labs Research a nd a Consulting Faculty Member in the Computer Science Department at Sta nford University. Kathleen’s research focuses on advancing the theory a nd practice of programming languages and on applying ideas from the prog ramming language community to the problem of ad hoc data management. Th e main thrust of her work has been in domain-specific languages to facil itate programming with massive amounts of ad hoc data\, including the Ha ncock system for efficiently building signatures from massive transactio n streams and the PADS system for managing ad hoc data. \;\n \;\nK athleen is an ACM Distinguished Scientist. She has served as program ch air for FOOL\, CUFP\, and ICFP. She is past Chair of the ACM Special Int erest Group in Programming Languages (SIGPLAN)\, Co-Chair of CRA’s Commi ttee on the Status of Women (CRA-W)\, and an editor of the Journal of Fu nctional Programming. She is currently serving on the CRA Board.\n\nImp orted from: http://calagator.org/events/1250458627 URL:http://www.galois.com/blog/2010/04/30/tech-talk-typing-directories/ SUMMARY:Galois Tech Talk: Typing Directories (NOTE THE DAY/TIME CHANGE!) LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100512T154907Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100518T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100518T103000 DTSTAMP;VALUE=DATE-TIME:20100512T154907Z LAST-MODIFIED;VALUE=DATE-TIME:20100512T154907Z UID:http://calagator.org/events/1250458682 DESCRIPTION:presenter: Mark Jones \;\n \;\nabstract: \;\nDevelop ers of systems software must often deal with low-level and performance-c ritical details that are hard to address in high-level programming langu ages. As a result\, much of the systems software that is produced today is written in languages like C and assembly code\, without the benefit o f more expressive type systems or other features from modern functional programming languages that could help to increase programmer productivit y or software quality. In this talk\, we present an update on the status of Habit\, a dialect of Haskell that we are designing\, as part of the HASP project at PSU\, to meet the needs of high assurance systems progra mming. Among other features\, Habit provides: mechanisms for fine contro l over representation of bit-level and memory-based data structures\; st rong support for both functional and imperative programming\; and a flex ible type system that allows precise characterization of size and bound information via type level naturals\, as well as termination properties resulting from the use of unpointed types.\n\nTags: functional programmi ng\, galois\, haskell\, systems programming\n\nImported from: http://cal agator.org/events/1250458682 URL:http://www.galois.com/blog/2010/05/12/tech-talk-developing-good-habit s-for-bare-metal-programming/ SUMMARY:Galois Tech Talk: Developing Good Habits for Bare-Metal Programmi ng 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:20100527T233301Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100603T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100603T103000 DTSTAMP;VALUE=DATE-TIME:20100527T233301Z LAST-MODIFIED;VALUE=DATE-TIME:20100527T233301Z UID:http://calagator.org/events/1250458728 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\nIMPO RTANT: Please note that this talk is Thursday. \;\n \;\ntitle: \;\n Categories are Databases \;\n \;\npresenter: \;\n D r. David Spivak \;\n \;\ntime: \;\n 10:30 am\, 03 June 2010 \, Thursday \;\n \;\nlocation \;\n Galois Inc. \;\n 4 21 SW 6th Ave. Suite 300\, Portland\, OR\, USA \;\n (3rd floor of the Commonwealth building) \;\n \;\nabstract: \;\n Category theory is a powerful language for organizing layers of abstraction in a ll areas of mathematics. Databases are powerful tools for organizing inf ormation of all sorts. Whereas categories are often considered hopelessl y abstract\, databases are often considered horrifically mundane. Thus i t is either strange or fitting that\, mathematically speaking\, categori es and databases are the same concept. In this talk I’ll show how to tur n any database into a category and any category into a database. I’ll al so discuss functors and how they may be useful for issues of data migrat ion and merging. \;\n \;\nbio: \;\n David Spivak graduated w ith a PhD in mathematics from UC Berkeley in 2007\; his thesis used high er category theory to fix an old problem in geometry. From 2007 to the p resent\, he have been a postdoc at the University of Oregon in the Math Department. During this time\, his focus has moved toward the idea of us ing category theory to understand information and communication. This s ummer\, he will become a mathematics postdoc at MIT for three years\, fo cusing on information and communication from a category-theoretic perspe ctive. \n\nImported from: http://calagator.org/events/1250458728 URL:http://www.galois.com/blog/2010/05/27/tech-talk-categories-are-databa ses/ SUMMARY:Tech Talk: Categories are Databases LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100604T002257Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100608T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100608T103000 DTSTAMP;VALUE=DATE-TIME:20100604T002257Z LAST-MODIFIED;VALUE=DATE-TIME:20100604T002257Z UID:http://calagator.org/events/1250458746 DESCRIPTION:presenter: \;\nTaras Glek \;\n \;\nabstract: \;\n A competitive browser market requires fast-paced improvements to the cod ebase. Such improvements may require significant refactoring of large pa rts of the codebase. Mozilla Firefox is one of the largest open source C ++ projects. Unfortunately C++ is a complex language: method overloading \, virtual functions\, template instantiation\, pointer arithmetic\, etc reduce developer productivity. Mozilla developed C++ static analysis an d refactoring tools to increase developer leverage in C++. Static analys is is done via Dehydra/Treehydra GCC plugins and refactoring is accompli shed by extending the Elsa C++ parser. This talk will discuss why Mozill a needs static analysis\, why there are so few tools for C++\, and speci fic projects that we’ve embarked on.\n\nTags: galois\, open source\, sta tic analysis\n\nImported from: http://calagator.org/events/1250458746 URL:http://www.galois.com/blog/2010/06/03/tech-talk-large-scale-static-an alysis-at-mozilla/ SUMMARY:Galois Tech Talk: Large-Scale Static Analysis at Mozilla 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:20100623T234930Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100629T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100629T103000 DTSTAMP;VALUE=DATE-TIME:20100623T234930Z LAST-MODIFIED;VALUE=DATE-TIME:20100623T234930Z UID:http://calagator.org/events/1250458804 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\ntitl e: \;\n Towards a High-Assurance Runtime System: Certified Garbage Collection \;\n \;\npresenter: \;\n Andrew Tolmach \;\ n \;\ntime: \;\n 10:30am\, Tuesday\, 29 June 2010. \;\n \ ;\nlocation: \;\n Galois Inc. \;\n 421 SW 6th Ave. Suite 300 \, Portland\, OR\, \;\n USA \;\n (3rd floor of the Commonwea lth building) \;\n \;\nabstract: \;\n It seems obvious that the reliability of critical software can be improved by using high-leve l\, memory-safe languages (Haskell\, ML\, Java\, C#\, etc.). But most ex isting implementations of these languages rely on large\, complex run-ti me systems coded in C. Using such an RTS leads to a large "\;credibi lity gap"\; at the heart of the assurance argument for the overall s ystem. To fill this gap\, we are working to build a new high-assurance r un-time system (HARTS)\, using an approach grounded in machine-assisted verification\, with an initial focus on providing certifiably correct ga rbage collection.This talk will describe a machine-certified framework f or correct compilation and execution of programs in garbage-collected la nguages. Our framework extends Leroy's Coq-certified Compcert compiler a nd Cminor intermediate language. We add a new intermediate language\, GC minor\, that supports GC'ed languages and has a proven semantics-preserv ing translation to assembly code. GCminor neatly encapsulates the interf ace between mutator and collector code\, while remaining simple and flex ible enough to be used with a wide variety of source languages and colle ctor styles. Front ends targeting GCminor can be implemented using any c ompiler technology and any desired degree of verification\, including fu ll semantics preservation\, type preservation\, or informal trust. As an example application of our framework\, we describe a compiler for Haske ll that translates the GHC's Core intermediate language to GCminor. (Thi s is joint work with Andrew McCreight and Tim Chevalier.) \;\n \;\ nbio: \;\n Andrew Tolmach has been a faculty member at Portland St ate University since receiving his Ph.D.in Computer Science from Princet on in 1992. His current research interests\, pursued under the aegis of the PSU High Assurance Systems Programming (HASP) project\, focus on hig h-assurance systems software development\, in particular using formal ve rification. His past publications\, mostly about functional languages\, include work on operating systems in Haskell\, garbage collection\, comp ilation\, debugger implementation\, integration with logic languages\, a nd lazy functional algorithms. \n\nImported from: http://calagator.org/e vents/1250458804 URL:http://www.galois.com/blog/2010/06/23/tech-talk-towards-a-high-assura nce-runtime-system-certified-garbage-collection/ SUMMARY:Galois Tech Talk: Towards a High-Assurance Runtime System: Certif ied Garbage Collection LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100702T172233Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100709T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100709T103000 DTSTAMP;VALUE=DATE-TIME:20100702T172233Z LAST-MODIFIED;VALUE=DATE-TIME:20100702T172233Z UID:http://calagator.org/events/1250458823 DESCRIPTION:Requirements and Performance of Data Intensive\, Irregular Ap plications \;\n \;\nDr. John Feo \;\n \;\nMany fundamental s cience\, national security\, and business applications need to process l arge volumes of irregular\, unstructured data. Data collection and analy sis is rapidly changing the way the scientific\, national security\, and economic communities operate. There are worldwide operational deploymen ts of instruments to detect the proliferation of weapons of mass destruc tion\, monitor terrorist cells\, and track the movement of illicit goods and services. In the next 15 years 30% of battle-space defense forces w ill be autonomous with each advanced robotic device carrying dozens of s ophisticated sensors collecting\, processing\, analyzing and transmittin g large amounts of data. American economic competitiveness will depend i ncreasingly on the timely analysis of many Petabytes of data collected i n diverse computing clouds charting the social and economic behavior of consumers. \;\n \;\nUnlike traditional scientific applications bas ed on linear algebra routines\, data analytic applications comprise larg e\, integer-based graph computations with irregular data access patterns \, low computation to memory access ratios\, and high levels of fine gra in parallelism that pass data and synchronize frequently. Traditional ar chitectures optimized to run large-scale floating point intensive simula tions are inadequate\, and more suitable high-end architectures such as the Cray XMT are needed. In this talk I will discuss the programming lan guage\, tools\, and system requirements for data analytic applications. I will survey the research at PNNL’s Center for Adaptive Supercomputer S oftware as regards graph analytics. In particular\, I will present sever al key graph algorithms we have developed with an emphasis on structure\ , use of special hardware features\, performance\, and scalability.\n\nT ags: galois\, graph algorithm\n\nImported from: http://calagator.org/eve nts/1250458823 URL:http://www.galois.com/blog/2010/07/02/tech-talk-requirements-and-perf ormance-of-data-intensive-irregular-applications/ SUMMARY:Galois Tech Talk: Requirements and Performance of Data Intensive\ , Irregular Applications LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100727T184602Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100803T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100803T103000 DTSTAMP;VALUE=DATE-TIME:20100727T184602Z LAST-MODIFIED;VALUE=DATE-TIME:20100727T184602Z UID:http://calagator.org/events/1250458930 DESCRIPTION:Galois is pleased to host the following tech talk. These tal ks are open to the interested public. Please join us! \;\n \;\nti tle: \;\n Industrial Strength Distributed Explicit Model Checking& #13\;\n \;\npresenter: \;\n John Erickson \;\n \;\ntime:& #13\;\n 10:30am\, August 3rd\, 2010 \;\n \;\nlocation: \;\n Galois Inc. \;\n 421 SW 6th Ave. Suite 300\, Portland\, OR\, U SA \;\n (3rd floor of the Commonwealth building) \;\n \;\nA bstract: \;\n We present PReach\, an industrial strength distribut ed explicit state model checker based on Murphi. The goal of this projec t was to develop a reliable\, easy to maintain\, scalable model checker that was compatible with the Murphi specification language. PReach is im plemented in the concurrent functional language Erlang\, chosen for its parallel programming elegance. We use the original Murphi front-end to p arse the model description\, a layer written in Erlang to handle the com munication aspects of the algorithm\, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean an d simple implementation\, with the core parallel algorithms written in u nder 1000 lines of code. This talk describes the PReach implementation i ncluding the various features that are necessary for the large models we target. We have used PReach to model check an industrial cache coherenc e protocol with approximately 30 billion states. To our knowledge\, this is the largest number published for a distributed explicit state model checker. PReach has been released to the public under an open source BSD license. \;\n \;\nbio: \;\n John Erickson is a Design Engin eer at Intel Hillsboro. He graduated with his PhD in Computer Science f rom The University of Texas at Austin in 2008. Currently he is working on the validation of uncore components in a 50+ core processor using a v ariety of formal and dynamic techniques. Past research interests include theorem proving with a focus on lemma generation and generalization in the context of induction. \n\nImported from: http://calagator.org/events /1250458930 URL:http://www.galois.com/blog/2010/07/27/industrial-strength-distributed -explicit-model-checking/ SUMMARY:Galois Tech Talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100811T185129Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100817T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100817T103000 DTSTAMP;VALUE=DATE-TIME:20100811T185129Z LAST-MODIFIED;VALUE=DATE-TIME:20100811T185129Z UID:http://calagator.org/events/1250458996 DESCRIPTION:Computers As We Don’t Know Them \;\nChristof Teuscher\, Ph D \;\n \;\nSince the beginning of modern computer science some six ty years ago\, \;\nwe are building computers in pretty much the same way. Silicon \;\ntransistor electronics serves as a physical device\, the von Neumann \;\narchitecture provides a computer design model\, while the abstract \;\nTuring machine concept supports the theoretica l foundations. However\, \;\nin recent years\, unimagined computing d evices have seen the light \;\nbecause of advances in synthetic biolo gy\, nanotechnology\, material \;\nscience\, and neuroscience. Many o f these novel devices share the \;\nfollowing characteristics: (1) th ey are made up from massive numbers \;\nof simple\, stochastic compon ents which (2) are embedded in 2D or 3D \;\nspace in some disordered way. A grand challenge in consists in \;\ndeveloping computing paradi gms\, design methodologies\, formal \;\nframeworks\, architectures\, and tools that allow to reliably compute \;\nand efficiently solve pr oblems with such devices. In this talk\, I will \;\noutline my vision ary and long-term research efforts to address the \;\ngrand challenge of building\, organizing\, and programming future \;\ncomputing mach ines. First\, I will review exemplary future and emerging \;\ncomputi ng devices and highlight the particular challenges that arise \;\nfor performing computations them. I will then delineate potential \;\nso lutions on how these challenges might be addressed. Self-assembled \; \nnano-scale cellular automata (CAs) and random boolean networks (RBNs)& #13\;\nwill serve as a simple showcase. I will also present the efforts& #13\;\nunderway to self-assemble massive-scale nanowire-based interconne ct \;\nfabrics for spatial computers and what the challenges are in t erms of \;\ncomputations and communication in such a non-classical sy stem. \;\n\n\nTags: galois\, tech talk\, technology\n\nImported from: http://calagator.org/events/1250458996 URL:http://www.galois.com/blog/2010/08/11/tech-talk-computers-as-we-dont- know-them/ SUMMARY:Galois Tech talk: Computers As We Don’t Know Them LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100819T222506Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100824T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100824T103000 DTSTAMP;VALUE=DATE-TIME:20100819T222506Z LAST-MODIFIED;VALUE=DATE-TIME:20100819T232502Z UID:http://calagator.org/events/1250459142 DESCRIPTION:abcBridge: Functional interfaces for AIGs and SAT solving \;\n \;\nEdward Z. Yang \;\n \;\nSAT solvers are perhaps the mo st under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most hu man generated NP-complete problems in time for lunch\, and there are man y\, many practical problem domains which involve NP-complete problems. H owever\, a major roadblock to using a SAT solver in your every day routi ne is translating your problem into SAT\, and then running it on a highl y optimized SAT solver\, which is probably implemented in C or C++ and n ot your usual favorite programming language. \;\n \;\nThis talk is about the use\, design and implementation of abcBridge\, a set of Haske ll bindings for ABC\, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC lo oks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs)\, are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.\n\nTags: galois\, tech talk\, functional programming\, open source\n\nImported from: http://calagator.org/events/1250459142 URL:http://www.galois.com/blog/2010/08/19/tech-talk-abcbridge-functional- interfaces-for-aigs-and-sat-solving/ SUMMARY:Galois Tech talk: abcBridge: Functional interfaces for AIGs and S AT solving LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100930T214250Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101005T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101005T103000 DTSTAMP;VALUE=DATE-TIME:20100930T214250Z LAST-MODIFIED;VALUE=DATE-TIME:20100930T214250Z UID:http://calagator.org/events/1250459295 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\ntitl e: \;\n Enabling Portable Build Systems \;\n \;\nspeaker: 3\;\n Rogan Creswick\, Galois\, Inc. \;\n \;\ntime: \;\n 10:30am\, Tuesday 05 October 2010 \;\n \;\nlocation: \;\n Galo is Inc. \;\n 421 SW 6th Ave. Suite 300\, Portland\, OR\, USA \;\n (3rd floor of the Commonwealth building) \;\n \;\nabstract: \ ;\n Modern computing–and high-performance computing in particular–uti lizes a variety of hardware and software platforms. These differences ma ke it difficult to develop build systems that are robust to platform cha nges. Our goal is to investigate the design of portable build systems th at are simple yet sufficiently robust with respect to environmental chan ges so that software can be easily distributed and built on\, and for\, myriad systems. We will discuss the current state of build tools and pre sent options for iteratively improving the reliability and utility of ex isting build tools while laying the groundwork for more sophisticated an d flexible build systems in the future. \;\n \;\nbio: \;\n Rogan Creswick joined Galois in January of 2010\, bringing expertise in programming by demonstration and natural language processing. He also ha rbors a love for tool development that is backed by years of academic re search in usability and software engineering at Oregon State University. His work in those areas improved techniques for fault location\, detect ion\, and assertion propagation in end-user programming languages. \n\nI mported from: http://calagator.org/events/1250459295 URL:http://www.galois.com/blog/2010/09/30/tech-talk-enabling-portable-bui ld-systems/ SUMMARY:Galois Tech Talk: Enabling Portable Build Systems LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20101005T221637Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101008T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101008T103000 DTSTAMP;VALUE=DATE-TIME:20101005T221637Z LAST-MODIFIED;VALUE=DATE-TIME:20101005T221637Z UID:http://calagator.org/events/1250459314 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\nPlea se note the nonstandard day/time! \;\n \;\ntitle: \;\n Intro duction to Logic Synthesis \;\n \;\nspeaker: \;\n Alan Mishc henko\, University of California\, Berkeley \;\n \;\ntime: \;\ n 10:30am\, Friday 08 October 2010 \;\n \;\nlocation: \;\n Galois Inc. \;\n 421 SW 6th Ave. Suite 300\, Portland\, OR\, USA \;\n (3rd floor of the Commonwealth building) \;\n \;\nabstract:& #13\;\n The lecture describes the problems solved by logic synthesis. It presents functional representations and typical computations applied to Boolean networks\, such as traversal\, windowing\, cut computation\, simulation\, Boolean reasoning. Presented next are And-Inverter Graphs (AIGs) that are increasingly used as a unifying representation for all p roblems. The lecture is finished by an overview of AIG-based solutions i n synthesis\, technology mapping\, and formal verification. \;\n \;\nbio: \;\n Alan Mishchenko graduated from Moscow Institute of P hysics and Technology\, Moscow\, Russia\, in 1993\, and received his Ph. D. degree from Glushkov Institute of Cybernetics\, Kiev\, Ukraine\, in 1 997. He has been a research scientist in the US since 1998. Currently\, Alan is an Associate Researcher at University of California\, Berkeley. His research interests are in developing computationally efficient met hods for logic synthesis and verification. \n\nImported from: http://cal agator.org/events/1250459314 URL:http://www.galois.com/blog/2010/10/05/galois-tech-talk-introduction-t o-logic-synthesis/ SUMMARY:Galois Tech Talk: Introduction to Logic Synthesis LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20101007T210527Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101012T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101012T103000 DTSTAMP;VALUE=DATE-TIME:20101007T210527Z LAST-MODIFIED;VALUE=DATE-TIME:20101007T210527Z UID:http://calagator.org/events/1250459326 DESCRIPTION:Presented by Priyank Kalla. \;\n \;\nApplications in Cr yptography require multiplication and exponentiation operations to be pe rformed over Galois fields GF(2^k). Therefore\, there has been quite an interest in the hardware design and optimization of such multipliers. Th is has led to impressive advancements in this area — such as the use of composite field decomposition techniques\, use of Montgomery multiplicat ion\, among others. \;\n \;\nMy research group has recently begun investigations in the verification of such Galois Field multipliers. Unf ortunately\, the word-length (k) in such multipliers can be very large: typically\, k = 256. Due to such large word-lengths\, verification techn iques based on decision diagrams\, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques\, ma inly Groebner bases theory\, to tackle this problem. In this talk\, we w ill see why Groebner bases techniques look promising\, while at the same time also studying the challanges that have to be overcome.\n\nTags: ga lois\, tech talk\, cryptography\n\nImported from: http://calagator.org/e vents/1250459326 URL:http://www.galois.com/blog/2010/10/07/2007/ SUMMARY:Galois Tech Talk: Application of Computer Algebra Techniques in V erification of Galois Field Multipliers: Potential + Challenges LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20101013T184130Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101019T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101019T103000 DTSTAMP;VALUE=DATE-TIME:20101013T184130Z LAST-MODIFIED;VALUE=DATE-TIME:20101013T231420Z UID:http://calagator.org/events/1250459350 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public. Please join us! \;\n \;\ntitl e: \;\n Fides: Remote Anomaly-Based Cheat Detection Using Client E mulation \;\nspeaker: \;\n Prof. Wu-chang Feng \;\ntime: \;\n 10:30am\, Tuesday 19 October 2010 \;\nlocation: \;\n Ga lois Inc. \;\n 421 SW 6th Ave. Suite 300\, Portland\, OR\,USA \ ;\n (3rd floor of the Commonwealth building) \;\n \;\nabstract : \;\nAs a result of physically owning the client machine\, cheaters in online games currently have the upper-hand when it comes to avoiding detection. To address this problem and turn the table on cheaters\, this paper presents Fides\, an anomaly-based cheat detection approach that r emotely validates game execution. With Fides\, a server-side Controller specifies how and when a client-side Auditor measures the game. To accur ately validate measurements\, the Controller partially emulates the clie nt and collaborates with the server. This paper examines a range of chea t methods and initial measurements that counter them\, showing that a Fi des prototype is able to efficiently detect several existing cheats\, in cluding one state-of-the-art cheat that is advertised as undetectable.&# 13\;\n \;\nbio: \;\nWu-chang Feng is currently an Associate Profes sor in the Intel Systems and Networking Laboratory at Portland State Uni versity where he leads a research group in networking and security. Wu-c hang received his B.S. in 1992 from Penn State University and his M.S.E. and Ph.D. degrees in 1994 and 1999 from the University of Michigan. He was awarded the IEEE Communications Society 2003 William R. Bennett priz e as well as one of four prizes recognizing the Best IBM Research Papers in Computer Science\, Electrical Engineering and Math published in 2002 . \n\nImported from: http://calagator.org/events/1250459350 URL:http://www.galois.com/blog/2010/10/13/tech-talk-fides-remote-anomaly- based-cheat-detection-using-client-emulation/ SUMMARY:Galois Tech Talk: Fides: Remote Anomaly-Based Cheat Detection Usi ng Client Emulation LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20101018T205118Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101022T163000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101022T153000 DTSTAMP;VALUE=DATE-TIME:20101018T205118Z LAST-MODIFIED;VALUE=DATE-TIME:20101021T160319Z UID:http://calagator.org/events/1250459367 DESCRIPTION:presenter: David Spivak \;\n \;\nAbout five months ago I gave a talk here at Galois called “Databases are categories.” The basi c idea was that a database schema can be represented as a category C and its states can be represented as functors C–>\;Set. In this talk I’ll refine that notion a bit\, explaining that schemas are better represent ed as sketches. I’ll also show how\, within this model one can: deal wit h incomplete data\; incorporate typing and calculated fields\; and perfo rm queries\, define views\, and migrate data between disparate schemas. That is\, I’ll try to show that the categorical approach handles everyth ing one might hope it would. Finally\, I’ll discuss a linguistic version of categories\, called “ologs\,” and show how they may help to democrat ize information storage.\n\nTags: galois\, tech talk\, category theory\n \nImported from: http://calagator.org/events/1250459367 URL:http://www.galois.com/blog/2010/10/18/databases-are-categories-2-refi nements-and-extensions/ SUMMARY:Galois Tech Talk: Databases are Categories 2: Refinements and Ext ensions. LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 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:20101122T190423Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101130T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101130T103000 DTSTAMP;VALUE=DATE-TIME:20101122T190423Z LAST-MODIFIED;VALUE=DATE-TIME:20101122T190423Z UID:http://calagator.org/events/1250459490 DESCRIPTION:Presented by Brian Ford \;\n \;\nRuby is a highly dynam ic\, strongly-typed programming language created by Yukihiro Matsumoto i n 1993 and first released in 1995. It borrows from Smalltalk\, Lisp\, an d Perl. Ruby has single inheritance\, mixins\, and syntax features like omission of parentheses that make it well-suited for embedded domain-spe cific languages. Ruby was popularized by the Ruby on Rails web developme nt framework. \;\n \;\nThe Rubinius project began as an implementa tion of the Ruby programming language roughly following the design of th e Smalltalk-80 virtual machine described in the Blue book (“Smalltalk-80 : the language and its implementation” by Adele Goldberg and David Robso n). We have extended the initial implementation based on modern research in virtual machines\, garbage collectors\, and just-in-time (JIT) compi lers. Rubinius currently features a stack-oriented opcode virtual machin e\, generational garbage collector\, and LLVM-based JIT compiler. Most o f the Ruby core library and the bytecode compiler are written in Ruby.&# 13\;\n \;\nWe will examine the main features of Rubinius and take a d eeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load\, startup \, and suitability for using Rubinius in Android phones. If there is tim e and interest\, we will discuss implementing programming languages besi des Ruby on Rubinius.\n\nTags: galois\, tech talk\, ruby\, rubinius\, op en source\n\nImported from: http://calagator.org/events/1250459490 URL:http://www.galois.com/blog/2010/11/22/tech-talk-the-rubinius-virtual- machine/ SUMMARY:Galois Tech Talk: The Rubinius Virtual Machine LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110105T004721Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110111T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110111T103000 DTSTAMP;VALUE=DATE-TIME:20110105T004721Z LAST-MODIFIED;VALUE=DATE-TIME:20110105T004721Z UID:http://calagator.org/events/1250459584 DESCRIPTION:Presented by Rebekah Leslie. \;\n \;\nThe existing impl ementation of DDT uses a depth-first search algorithm to drive the explo ration of new paths for testing. This algorithm provides full coverage o f the program under test\, but is limited by the fact that the number of paths increases exponentially with the size of the program. By employin g the control-flow graph information of the program under test\, we can direct the testing process towards program paths that contain unvisited points and therefore obtain full branch coverage in a smaller number of tests than would be required by the original depth-first search algorith m. We will present two uses of control-flow graph information in DDT. Th e first use is a refinement of depth-first search where control-flow gra ph information is used to prune the search space to eliminate unnecessar y tests. The second use is in the context of a prioritized work-queue th at forms the basis for a variety of sophisticated search algorithms that exploit different heuristics.\n\nTags: galois\, tech talk\, ddt\, debug ging\n\nImported from: http://calagator.org/events/1250459584 URL:http://corp.galois.com/blog/2011/1/4/tech-talk-control-flow-graph-gui ded-exploration-in-ddt.html SUMMARY:Galois Tech Talk: Control-flow Graph Guided Exploration in DDT 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:20110126T230643Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110201T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110201T103000 DTSTAMP;VALUE=DATE-TIME:20110126T230643Z LAST-MODIFIED;VALUE=DATE-TIME:20110126T230643Z UID:http://calagator.org/events/1250459683 DESCRIPTION:Presented by Simon Winwood. \;\n \;\nIn 2009 the NICTA L4.verified project completed the machine-checked correctness proof of t he seL4 microkernel. The natural next step is then to use this verified kernel to construct verified systems. \;\n \;\nIn this talk I give an overview of the ongoing work into systems verification in the Trustw orthy Embedded Systems project. In particular\, I will focus on the use of access control results to reason about the properties of systems in t he presence of large untrusted components\, such as a Linux kernel. \ ;\n\n\nTags: galois\, tech talk\, l4\, os\n\nImported from: http://calag ator.org/events/1250459683 URL:http://corp.galois.com/blog/2011/1/26/tech-talk-verifying-sel4-based- systems.html SUMMARY:Galois Tech talk: Verifying seL4-based Systems 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:20110208T232607Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110215T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110215T103000 DTSTAMP;VALUE=DATE-TIME:20110208T232607Z LAST-MODIFIED;VALUE=DATE-TIME:20110208T232607Z UID:http://calagator.org/events/1250459772 DESCRIPTION:Presented by Johan Tibell. \;\n \;\nThe most commonly u sed map (dictionary) data type in Haskell is implemented using a size ba lanced tree. While size balanced trees provide good asymptotic performan ce\, their real world performance is not stellar\, especially when used with keys which are expensive to compare\, such as strings. \;\n \ ;\nIn this talk we will look at two different map implementations that u se hashing to achieve better real world performance. The implementations have different performance characteristics: one provides very fast look -ups while the other trades better insert performance for somewhat slowe r look-ups. I will describe the design of these data structures and show some early benchmark results.\n\nTags: galois\, tech talk\, haskell\, d ata structures\n\nImported from: http://calagator.org/events/1250459772 URL:http://corp.galois.com/blog/2011/2/8/tech-talk-faster-persistent-data -structures-through-hashing.html SUMMARY:Galois Tech Talk: Faster Persistent Data Structures Through Hashi ng LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110217T175444Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110222T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110222T103000 DTSTAMP;VALUE=DATE-TIME:20110217T175444Z LAST-MODIFIED;VALUE=DATE-TIME:20110217T175444Z UID:http://calagator.org/events/1250459809 DESCRIPTION:Presented by Rachel Lanigan. \;\n \;\nEngineers Without Borders USA is a fast-growing national non-profit impacting developing communities around the world. EWB provides an opportunity for engineerin g students and professionals to use their skills to develop sustainable\ , appropriate technologies for specific applications\, to help meet the basic needs of people. Our programs typically start with a focus on prov iding water and sanitation\, but often move into other areas depending o n the needs of the people. There is a role for everyone at EWB\, from en gineers to public health professionals. Rachel will give a background on EWB\, our local chapter\, and how to get involved.\n\nTags: galois\, te ch talk\, community\, ewb\n\nImported from: http://calagator.org/events/ 1250459809 URL:http://corp.galois.com/blog/2011/2/17/tech-talk-engineers-without-bor ders.html SUMMARY:Galois tech talk: Engineers Without Borders LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110308T180357Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110315T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110315T103000 DTSTAMP;VALUE=DATE-TIME:20110308T180357Z LAST-MODIFIED;VALUE=DATE-TIME:20110308T180357Z UID:http://calagator.org/events/1250459894 DESCRIPTION:Presented by Philip Weaver. \;\n \;\nJanrain offers use r management services that include single sign-on\, social login\, and p rofile storage. We have recently begun using Haskell extensively to impl ement our products\, and would like to share what the experience has bee n like. \;\n \;\nIn this talk we will give a technical demonstrati on of Capture\, whose backend is written in Haskell\, discuss some of th e implementation details of Capture\, and look at some of the joys and p itfalls that we experienced.\n\nTags: galois\, tech talk\, haskell\, web services\n\nImported from: http://calagator.org/events/1250459894 URL:http://corp.galois.com/blog/2011/3/8/tech-talk-haskell-and-the-social -web.html SUMMARY:Galois Tech Talk: Haskell And The Social Web LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 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:20110412T230459Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110419T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110419T103000 DTSTAMP;VALUE=DATE-TIME:20110412T230459Z LAST-MODIFIED;VALUE=DATE-TIME:20110412T230459Z UID:http://calagator.org/events/1250460480 DESCRIPTION:Presented by Jim Snow. \;\n \;\nRNA Networks is a softw are company focused on providing the next generation storage cache solut ion that addresses performance deficiencies and the rising cost of stora ge for virtual environments. Our software solution utilizes compute reso urces (DRAM and flash) as a distributed clustered cache moving 'active' data off of the storage tier and into the compute tier translating to si gnificant performance gains with no additional investment in hardware re sources. RNA's MVX technology is based on a distributed shared memory co re that leverages RDMA fabrics and allows for a unified and flexible nam espace that can scale proportionally to meet any performance or capacity need. \;\n \;\nIn this presentation we'll discuss the core archit ecture and how this can be leveraged to both reduce the cost of high end storage and meet high performance storage objectives.\n\nTags: galois\, tech talk\, operating systems\, shared memroy\n\nImported from: http:// calagator.org/events/1250460480 URL:http://corp.galois.com/blog/2011/4/12/tech-talk-using-rna-mvx-shared- memory-pools-to-improve-large.html SUMMARY:Galois Tech Talk: Using RNA MVX Shared Memory Pools to Improve La rge-Memory Workloads and Storage Performance LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110504T224356Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110510T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110510T103000 DTSTAMP;VALUE=DATE-TIME:20110504T224356Z LAST-MODIFIED;VALUE=DATE-TIME:20110504T224356Z UID:http://calagator.org/events/1250460560 DESCRIPTION:Presented by Chad Scherrer. \;\n \;\nSampling from a la rge discrete distribution is a common problem in statistics. In this tal k\, we'll consider a real-world situation where the properties of the di stribution cause common approaches to break down\, and we'll arrive at a Haskell-based solution that fixes the problem.\n\nTags: galois\, tech t alk\, haskell\, statistics\n\nImported from: http://calagator.org/events /1250460560 URL:http://corp.galois.com/blog/2011/5/4/tech-talk-empirical-sampling-wit h-haskell.html SUMMARY:Galois Tech Talk: Empirical Sampling With Haskell LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110527T173614Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110603T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110603T103000 DTSTAMP;VALUE=DATE-TIME:20110527T173614Z LAST-MODIFIED;VALUE=DATE-TIME:20110527T173659Z UID:http://calagator.org/events/1250460654 DESCRIPTION:Presented by Nicholas Begley\, Dave Dung Anh\, James Heilinge r\, Alec Rasmussen\, and Mark Theuson. \;\n \;\nIt's a bird! It's a plane! No\, it's an open-source autonomous quad-copter. In collaborati on with the Portland State University Electrical and Computer Engineerin g Dept.\, Galois mentored a Spring semester Senior Capstone Project to b uild an ArduCopter. The ArduCopter is based on the Arduino open-source h ardware platform\, and includes infrared sensors (collision avoidance)\, sonar and barometer (altitude hold)\, GPS (location)\, magnetometer (di rection)\, and gyro (stabilization). This talk will include a descriptio n of the ArduCopter and it's operation\, including the trials and tribul ations of building and testing one. Of course\, the talk will include co ol videos.\n\nTags: galois\, tech talk\, psu\, quad-copter\, technology\ n\nImported from: http://calagator.org/events/1250460654 URL:http://corp.galois.com/blog/2011/5/27/tech-talk-building-an-open-sour ce-autonomous-quad-copter.html SUMMARY:(Friday) Galois Tech talk: Building an Open-Source Autonomous Qu ad-Copter LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20110613T170841Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110618T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110618T093000 DTSTAMP;VALUE=DATE-TIME:20110613T170841Z LAST-MODIFIED;VALUE=DATE-TIME:20110613T170841Z UID:http://calagator.org/events/1250460712 DESCRIPTION:"\;Cfengine is an automation framework for system adminis tration or IT Management. It began in 1993 and\, after significant resea rch and evaluation\, it was completely rewritten in 2007. Today it is th e most advanced automation framework\, supporting all common platforms\, and designed with security in mind\, from the ground up."\; \;\n \;\nAleksey Tsalolikhin\, aleksey at verticalsysadmin.com\, made us an outstanding offer to introduce us to Cfengine version 3 the weekend f ollowing this year's USENIX conference. \;\n \;\nAfterward\, feel free to join us for lunch!\n\nTags: devops\, cfengine\n\nImported from: http://calagator.org/events/1250460712 URL:http://lists.pdxlinux.org/pipermail/plug/2011-June/072572.html SUMMARY:Cfengine 3 Introduction 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:20110714T200247Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110719T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110719T103000 DTSTAMP;VALUE=DATE-TIME:20110714T200247Z LAST-MODIFIED;VALUE=DATE-TIME:20110714T200247Z UID:http://calagator.org/events/1250460825 DESCRIPTION:Presented by Adam Foltzer. \;\n \;\nInterpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq\, where all recursive functions must provably terminate\, it is impossibl e to write interpreters for non-terminating languages. The standard alte rnative is to inductively define operational semantics\, but this can yi eld proofs that are difficult to automate\, particularly in the presence of changing language features. \;\n \;\nThis talk presents a comb ined approach\, where an interpreter is used in combination with operati onal semantics to prove type preservation of a small functional language . To demonstrate the scalability of the Coq development\, let expression s and a pair types will be added and preservation will be proved again w ith only one extra line of proof script. \;\n \;\nThis technique a nd development are adapted from Greg Morrisett's lectures at the 2011 Or egon Programming Languages Summer School\, and are available at his web site.\n\nTags: galois\, tech talk\, theorem proving\, coq\n\nImported fr om: http://calagator.org/events/1250460825 URL:http://corp.galois.com/blog/2011/7/14/tech-talk-combining-denotationa l-and-operational-semantics-f.html SUMMARY:Galois tech talk: Combining Denotational and Operational Semantic s for Scalable Proof Development 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:20110810T222023Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110816T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110816T103000 DTSTAMP;VALUE=DATE-TIME:20110810T222023Z LAST-MODIFIED;VALUE=DATE-TIME:20110810T222023Z UID:http://calagator.org/events/1250461208 DESCRIPTION:Presented by Sebastian Niller and Nis N. Wegmann \;\n \ ;\n#1 \;\ntitle: \;\nTranslation of Functionally Embedded Domain-s pecific Languages With Static Type Preservation by using Witnesses \; \n \;\nabstract: \;\nStatic type preservation automatically guaran tees type-correctness of an embedded domain-specific language (eDSL) by tying its type system to that of the host-language. Not only does this o bviate the need for a custom type checker\, it also preserves type-corre ctness during code transformations and optimizations\, and simplifies an d increases the efficiency of interpreters. When implementing a translat or from a source DSL with type preservation to a target DSL\, the common ly chosen approach requires the incorporation of extensions in the sourc e DSL specific to the target DSL\, which\, in cases where multiple back- ends are required\, obfuscates the source DSL and decreases the overall modularity. We show that by using witnesses\, a technique which facilita tes the construction of type-level proofs\, we can effectively cope with this issue and implement translators without extending the source DSL.& #13\;\n \;\nWe have applied our approach on Copilot\, a Haskell-embed ded domain specific language for runtime monitoring of hard real-time di stributed systems\, and used it for implementing two back-ends targeting the Haskell-embedded languages Atom and SBV. Our approach restrains to the Haskell 2010 Standard except for existentially and universally quant ified types. \;\n \;\n#2 \;\n \;\ntitle: \;\nFrom High-Le vel Languages to Monitoring Fault-Tolerant Hardware: Case-Studies of Run time Verification Using Copilot \;\n \;\nabstract: \;\nFailures of hard real-time systems can be caused by systematic faults in softwar e and hardware\, as well as by random hardware faults\, and faults due t o wear out of hardware components. Even if monitoring software is proven to comply to its specification\, there is no guarantee that failing und erlying hardware does not affect the monitors themselves. An application of distributed Copilot monitors to a redundant airspeed measurement sys tem is presented. We show the use of monitors enables the system to wit hstand benign and Byzantine hardware and software faults. \;\n \;\ nThe second part of the talk presents current work using Copilot \;\n to monitor the MAVLink protocol in flight of a sub-scale model \;\nof an Edge 540T aircraft.\n\nTags: galois\, tech talk\, haskell\, embedded systems\n\nImported from: http://calagator.org/events/1250461208 URL:http://corp.galois.com/blog/2011/8/10/tech-talks-back-to-back-talks-o n-haskell-and-embedded-system.html SUMMARY:Tech Talk: Back-to-back talks on Haskell and Embedded Systems 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:20110825T165716Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110830T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110830T103000 DTSTAMP;VALUE=DATE-TIME:20110825T165716Z LAST-MODIFIED;VALUE=DATE-TIME:20110825T165716Z UID:http://calagator.org/events/1250461242 DESCRIPTION:Presented by Kevin Butler \;\n \;\nThe complexity of mo dern operating systems makes securing them a challenging problem. Howeve r\, changes in the computing model\, such as the rise of cloud computing and smarter peripherals\, have presented opportunities to reconsider sy stem architectures\, as we move from traditional "\;stove-pipe"\ ; computing to distributed systems. In particular\, we can build trustwo rthy components that act to provide security in complex systems. \;\n \;\nThis talk discusses how new disk architectures may be exploited to aid the protection of systems by acting as policy decision and enforc ement points. We prototype disks that enforce data immutability at the b lock level on critical system data\, preventing malicious code from inse rting itself into system configuration and boot files. We then examine h ow storage may be used to ensure the integrity state of hosts prior to a llowing access to data\, and how such a design improves the security of portable storage devices. Using continual measurements of system state\, we show through formal reasoning that such a device enforces guarantees that data is read and written while the host is in a good state. Finall y\, we discuss some recent initiatives to assure the identity of the hos t and identify future directions for exploring the interface between sto rage and operating system security. \;\n\n\nTags: galois\, tech talk\ , security\n\nImported from: http://calagator.org/events/1250461242 URL:https://corp.galois.com/blog/2011/8/25/tech-talk-leveraging-emerging- storage-functionality-for-new.html SUMMARY:Galois Tech Talk: Leveraging Emerging Storage Functionality for N ew Security Services LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20111107T213344Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111110T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111110T103000 DTSTAMP;VALUE=DATE-TIME:20111107T213344Z LAST-MODIFIED;VALUE=DATE-TIME:20111107T213344Z UID:http://calagator.org/events/1250461554 DESCRIPTION:Presented by Dylan McNamee. \;\n \;\nThis talk is an i ntroduction to the MILS (Multiple Independent Layers \;\nof Security ) architecture\, motivated by the challenge of enforcing various kinds o f security policies. I'll describe the goals of policy enforcement\, tra ditional means of implementing security enforcement mechanisms\, and the emerging MILS architecture for enforcing policies with high assurance.\ n\nTags: galois\, architecture\, tech talk\, systems\, MILS\n\nImported from: http://calagator.org/events/1250461554 URL:http://corp.galois.com/blog/2011/11/7/tech-talk-enforcing-security-po licies-with-a-mils-architectu.html SUMMARY:Galois Tech Talk: Enforcing Security Policies with a MILS Archite cture LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20111110T194309Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111117T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111117T103000 DTSTAMP;VALUE=DATE-TIME:20111110T194309Z LAST-MODIFIED;VALUE=DATE-TIME:20111110T194309Z UID:http://calagator.org/events/1250461566 DESCRIPTION:Presented by Eric Migicovsky. \;\n \;\n Hardware is har d. At least that's what people always say. Building a hardware startup r equires a broad base of technical knowledge\, from electronics and manuf acturing experience to aesthetic and interface design. But Eric Migicovs ky chose to start a hardware company after graduating from engineering b ecause he wanted to see something he designed become a physical reality. \;\n \;\ninPulse is a $150 hackable Bluetooth smartwatch. It conn ects to your smartphone and displays notifications like incoming emails\ , calls\, and calendar alerts right on your wrist. After launching an SD K\, 3rd party developers have started to create apps for inPulse. \;\ n \;\nIn his talk\, Eric will share some honest stories and anecdotes from various stages of product development. He'll also talk about the c osts\, timeframes and failure modes of hardware startups.\n\nTags: start up\, galois\, hardware\, tech talk\n\nImported from: http://calagator.or g/events/1250461566 URL:https://corp.galois.com/blog/2011/11/10/tech-talk-candid-experiences- from-a-hardware-startup.html SUMMARY:Galois Tech Talk: Candid experiences from a hardware startup LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20111209T194146Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111215T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20111215T103000 DTSTAMP;VALUE=DATE-TIME:20111209T194146Z LAST-MODIFIED;VALUE=DATE-TIME:20221115T074450Z UID:http://calagator.org/events/1250461722 DESCRIPTION:Presented by Nate Foster. \;\n \;\nThe languages used t o program networks today lack \;\nmodern features. Programming them i s a complicated task\, and \;\noutages and infiltrations are frequent . We believe it is time to \;\ndevelop NETWORK PROGRAMMING LANGUAGES with the following \;\nessential features: \;\n \;\n* High-lev el abstractions that give programmers direct control \;\n over the n etwork\, allowing them to specify what they want the \;\n network to do without worrying about how to implement it. \;\n \;\n* Composi tional constructs that facilitate modular reasoning \;\n about progr ams. \;\n \;\n* Portability\, allowing programs written for one pl atform to be \;\n used with different devices. \;\n \;\n* Rigo rous semantic foundations that precisely document the \;\n meaning o f the language and provide a basis for building formal \;\n verifica tion tools. \;\n \;\nThe Frenetic language addresses these challe nges in the context \;\nof OpenFlow networks. It combines a streaming declarative query \;\nsub-language and a functional reactive sub-lan guage that\, \;\ntogether\, provide many of the features listed above . Our \;\nimplementation handles many low-level packet-processing det ails \;\nand keeps traffic in the "\;fast path"\; whenever po ssible.\n\nTags: galois\, networks\, tech talk\, programming languages\n \nImported from: http://calagator.org/events/1250461722 URL:http://corp.galois.com/blog/2011/12/9/tech-talk-frenetic-a-network-pr ogramming-language.html SUMMARY:Galois Tech Talk: Frenetic: A Network Programming Language LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:3 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:20120504T212553Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120511T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120511T103000 DTSTAMP;VALUE=DATE-TIME:20120504T212553Z LAST-MODIFIED;VALUE=DATE-TIME:20120504T212553Z UID:http://calagator.org/events/1250462359 DESCRIPTION:Presented by Charles Parker \;\n \;\nA basic problem in computer science is binary classification\, in which an algorithm appli es a binary label to data based on the presence or absence of some pheno menon. Problems of this type abound in areas as diverse as computational biology\, multimedia indexing\, and anomaly detection. Evaluating the p erformance of a binary labeling algorithm is itself a complex task\, oft en based on a domain-dependent notion of the relative cost of "\;fal se positives"\; versus "\;false negatives"\;. As these costs are often not available to researchers or engineers\, a number of metho ds are used to provide a cost-independent analysis of performance. In th is talk\, I will examine a number of these methods both theoretically an d experimentally. The presented results suggest a set of best practices for evaluating binary classification algorithms\, while questioning whet her a cost-independent analysis is even possible. \n\nTags: galois\, ana lysis\, tech talk\, algorithms\n\nImported from: http://calagator.org/ev ents/1250462359 URL:http://corp.galois.com/blog/2012/5/4/tech-talk-an-analysis-of-analysi s.html SUMMARY:Galois Tech Talk: An Analysis of Analysis LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120529T172402Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120605T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120605T103000 DTSTAMP;VALUE=DATE-TIME:20120529T172402Z LAST-MODIFIED;VALUE=DATE-TIME:20120529T172402Z UID:http://calagator.org/events/1250462410 DESCRIPTION:Presented by Chris Andrew\, Kayla Seliner\, Mark Craig\, and Trang Nguyen. \;\n \;\nOn October 7\, 2008\, the flight control s ystem of Qantas flight 72 malfunctioned without warning. The failure cau sed the aircraft to violently pitch down with an acceleration of -0.8g\, pitching passengers and crew into the roof of the cabin resulting in ma ny injuries. In the investigation that followed\, the malfunction was at tributed to a software problem in the Air Data Inertial Reference Unit. These units are utilized on all modern passenger jets\, but are propriet ary devices not open to public scrutiny. \;\n \;\nThis capstone pr oject develops an open source Air Data Inertial Reference Unit using fou r redundant Arduino boards each with a microcontroller\, 3D gyroscope an d accelerometer. Faults are injected into the system through software an d outputs are monitored over serial ports allowing the user to test effe ctiveness of fault-tolerant algorithms to mask fail silent and byzantine faults in the sensors. Failures in ADIRU systems are usually complex in nature and arise under very anomalous circumstances suggesting that fau lt-tolerant system design could benefit from the diverse testing and eva luation that can occur in an open source community. This project demonst rates the low entry-cost to building a fault-tolerant system for open-so urce design and experimentation.\n\nTags: galois\, monitoring\, tech tal k\, fault tolerance\n\nImported from: http://calagator.org/events/125046 2410 URL:http://corp.galois.com/blog/2012/5/29/why-do-airplanes-crash-building -an-open-source-aircraft-sens.html SUMMARY:Why Do Airplanes Crash? Building an Open-Source Aircraft Sensor S ystem LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120628T203737Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120628T150000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120628T140000 DTSTAMP;VALUE=DATE-TIME:20120628T203737Z LAST-MODIFIED;VALUE=DATE-TIME:20120628T203737Z UID:http://calagator.org/events/1250462512 DESCRIPTION:Presented by Sergio Antoy from Portland State University. 3\;\n \;\nIn this talk\, I will introduce narrowing\, the characteriz ing feature of functional logic programming\, from the programmer's viep oint. Narrowing promotes non-determinism and it enables computing with i ncomplete or unknown information. After a short and informal presentatio n of Curry\, the leading functional logic language\, I will discuss a fe w examples showing that narrowing and its associated non-determinism sup port programming at a very high level of abstraction.\n\nTags: programmi ng\, galois\, tech talk\, paradigms\n\nImported from: http://calagator.o rg/events/1250462512 URL:http://corp.galois.com/blog/2012/6/28/tech-talk-programming-with-narr owing.html SUMMARY:Galois Tech Talk: Programming with Narrowing LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120725T171413Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120802T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120802T103000 DTSTAMP;VALUE=DATE-TIME:20120725T171413Z LAST-MODIFIED;VALUE=DATE-TIME:20120725T171413Z UID:http://calagator.org/events/1250462652 DESCRIPTION:Presented by Iulian Neamtiu. \;\n \;\nThe relative nove lty and rapid evolution pace of the Android ecosystem (platform\, vendor -installed apps and third-party apps) means both the platform and apps r eceive little scrutiny. Hence there is a need for tools that assess\, mo nitor and verify all components of the Android ecosystem. This lack of t ools and scrutiny is particularly problematic when combined with the ope n nature of Google Play\, the main app distribution channel. \;\n \;\nIn the first part of this talk we will focus on multi-layer profilin g of Android apps using ProfileDroid\, a tool and framework we developed at UC Riverside. ProfileDroid is useful for a variety of Android app an alyses\, from performance to usability to security. ProfileDroid monitor s and correlates the behavior of an app at four layers: (a) static\, or app specification (b) user interaction\, (c) operating system\, and (d) network layer. Using ProfileDroid on 27 free and paid Android apps\, we have revealed: (a) discrepancies between the app specification and app e xecution\, (b) free versions of apps could end up costing more than thei r paid counterparts\, due to an order of magnitude increase in traffic\, (c) most network traffic is not encrypted\, (d) apps communicate with m any more sources than users might expect. \;\n \;\nIn the second p art of the talk we will present results from our long-term permission ev olution study of the Android ecosystem---platform and 237 apps---over th ree years. We found that the platform has increased the number of danger ous permissions and does not move towards finer-grained permissions\, an d that app developers do not follow the principle of least privilege. We will also briefly discuss our efforts with static information flow trac king for Android apps\, as well as building a log-and-replay system for Android.\n\nTags: security\, galois\, mobile\, android\, analysis\, tech talk\n\nImported from: http://calagator.org/events/1250462652 URL:http://corp.galois.com/blog/2012/7/25/tech-talk-comprehensive-analysi s-of-the-android-ecosystem.html SUMMARY:Galois Tech Talk: Comprehensive Analysis of the Android Ecosystem LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120821T181515Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120828T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120828T103000 DTSTAMP;VALUE=DATE-TIME:20120821T181515Z LAST-MODIFIED;VALUE=DATE-TIME:20120821T181515Z UID:http://calagator.org/events/1250462761 DESCRIPTION:Presented by Larry Diehl. \;\n \;\nMany advanced branch es of mathematics involve structures that abstract over well known speci fic instances\, e.g. abstract algebraic structures\, equivalence relatio ns\, various orders\, category theoretic structures\, etc. In typed func tional programming (e.g. with type classes in Haskell)\, encoding such s tructures amounts to enforcing the definition of elements and operations for a particular structure instance on one hand\, and being able to use said elements and operations in generic definitions on the other hand. With Dependently Typed Programming (DTP) we can go one step further and define propositions/properties for abstract structures\, and subsequentl y require proofs in particular instances. \;\n \;\nThis talk will tell the story of how examples of particular instances inspire an abstra ct definition (including its propositional properties)\, how to then ins tantiate the original concrete examples in the new abstract definition\, and finally create further abstract definitions that depend on previous ly defined ones. Emphasis will be given on how easily concrete proofs ca n be used as evidence for abstract propositions\, and how proofs about a bstract structures parameterized by other abstract structures may reuse their proofs (similar to the more common concept of reusing operations i n subsequent abstract definitions). The talk will use Agda as its demons tration language\, but proofs will mostly be in the form of equational r easoning that should look familiar to the non-expert.\n\nTags: programmi ng\, galois\, tech talk\, dependent types\n\nImported from: http://calag ator.org/events/1250462761 URL:http://corp.galois.com/blog/2012/8/21/tech-talk-abstract-anything-the ory-and-proof-reuse-via-dtp.html SUMMARY:Galois Tech Talk: Abstract "Anything": Theory and Proof Reuse via DTP LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 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:20121129T191942Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121204T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121204T103000 DTSTAMP;VALUE=DATE-TIME:20121129T191942Z LAST-MODIFIED;VALUE=DATE-TIME:20121129T191942Z UID:http://calagator.org/events/1250463146 DESCRIPTION:Presented by Becky Straus. \;\n \;\nAbstract: \;\nEf forts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) hav e attracted widespread attention and criticism\, and rightly so. But Was hington\, D.C. is far from the only place that officials are making deci sions that impact the privacy and free speech rights. State and local of ficials are jumping into the fray as well\, passing laws or creating pol icies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up wit h emerging technologies. This presentation will survey several areas whe re state and local officials in Oregon have recently been active\, inclu ding reviewing policies on automated license plate recognition\, surveil lance cameras\, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.\n\nTags: technology\, community\, privac y\, Galois tech talk\n\nImported from: http://calagator.org/events/12504 63146 URL:https://corp.galois.com/blog/2012/11/29/tech-talk-computers-and-priva cy-aclu-of-oregon-discusses-the.html SUMMARY:Galois tech talk: Computers and privacy\, ACLU of Oregon discusse s their 2013 agenda LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20121218T201510Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130117T200000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130117T180000 DTSTAMP;VALUE=DATE-TIME:20121218T201510Z LAST-MODIFIED;VALUE=DATE-TIME:20130109T233659Z UID:http://calagator.org/events/1250463246 DESCRIPTION:Come join the Portland Drone Enthusiast community for our mon thly meeting. If you like Drones\, UAVs\, or UAS then this is the group for you. We'll have some great guest speakers and the retreat to a local brewpub for continued discussion! \;\n \;\n* Mike Hutt\, UAS Prog ram Manager\, USGS National UAS Project Office \;\nMike will join us remotely to talk about how the US Geological Society is using UAS to sup port their missions. The UAS office currently flies the Raven\, Global H awk and T-Hawk to operate their missions. \;\n \;\n* Pat Hickey\, Mavelous Developer \;\nPat will speak about running ArduPilot and Ard uCopter on the new PX4 hardware\, and the advantages and challenges the new architecture brings with it. \;\n\n\nTags: drones\, plancast:plan =fgzl\n\nImported from: http://calagator.org/events/1250463246 URL:http://droneenthusiast.com/pdxdrones-january-meeting/ SUMMARY:PDXDrones January Meetup LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:4 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:20130307T165338Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130312T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130312T103000 DTSTAMP;VALUE=DATE-TIME:20130307T165338Z LAST-MODIFIED;VALUE=DATE-TIME:20130307T165338Z UID:http://calagator.org/events/1250463783 DESCRIPTION:Presented by Erlend Hamberg. \;\n \;\nAn important prob lem in genetics is phylogenetic inference: Coming up with good hypothese s for the evolutionary relationship between species – usually represente d as a “family tree”. As the amount of molecular data (e.g. DNA sequence s) quickly grows\, efficient algorithms become increasingly important to analyze this data. A maximum-likelihood approach with models for nucleo tide evolution allows us to use all the sequence data\, but is a computa tionally expensive approach. The number of possible trees also grows rap idly as we include more species. It is therefore necessary to use heuris tic search methods to find good hypotheses for the “true” tree. Evolutio nary algorithms (EA) is a class of such search/optimization algorithms t hat has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecula r data.\n\nTags: galois\, tech talk\, algorithms\, classification\n\nImp orted from: http://calagator.org/events/1250463783 URL:https://corp.galois.com/blog/2013/3/7/tech-talk-inferring-phylogenies -using-evolutionary-algorithm.html SUMMARY:Galois Tech Talk: Inferring Phylogenies Using Evolutionary Algori thms LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130404T004108Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130409T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130409T103000 DTSTAMP;VALUE=DATE-TIME:20130404T004108Z LAST-MODIFIED;VALUE=DATE-TIME:20130404T004108Z UID:http://calagator.org/events/1250463961 DESCRIPTION:Presented by Andrew Farmer. \;\n \;\nThe importance of reasoning about and refactoring programs is a central tenet of functiona l programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks\, leaving the programmer to do them by hand. This talk introduces HERMIT\, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Ha skell Compiler's optimization pipeline. With HERMIT\, users can experime nt with optimizations and equational reasoning\, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT\, demonstrate its use on exam ples\, and seek input for further development and case studies.\n\nTags: galois\, functional programming\, tech talk\, program transformation\n\ nImported from: http://calagator.org/events/1250463961 URL:https://corp.galois.com/blog/2013/4/3/tech-talk-introducing-hermit-a- plugin-for-transforming-ghc-c.html SUMMARY:Galois Tech Talk: Introducing HERMIT: A Plugin for Transforming G HC Core Language Programs LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130423T190226Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130430T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130430T103000 DTSTAMP;VALUE=DATE-TIME:20130423T190226Z LAST-MODIFIED;VALUE=DATE-TIME:20130423T190414Z UID:http://calagator.org/events/1250464090 DESCRIPTION:Presented by Joe FitzPatrick. \;\n \;\nGenerally\, ther e is a very low barrier to entry when it comes to software or network-ba sed attacks due to the fact that actual costs are minimal and most resou rces are readily available. This does mean that it's generally much easi er to attack the software of a system than the hardware\, but unfortunat ely that also leads to overconfidence in\, as well as misplaced trust in hardware. \;\n \;\nThere is a clear 'hierarchy of attacks' in the hardware world. There are costs\, often significant\, involved in acqui ring your hardware 'target' which might be damaged or destroyed in the p rocess. There are a number of useful tools that cost anywhere from a few dollars to a few million dollars. I'll give a couple examples of what's possible within budgets of $100\, $10\,000\, and $1\,000\,000. I'll poi nt out how many capabilities are much more accessible than most assume\, and how vulnerable to sub-$100 attacks most of our 'secure' hardware re ally is.\n\nTags: security\, galois\, tech talk\n\nImported from: http:/ /calagator.org/events/1250464090 URL:http://corp.galois.com/blog/2013/4/23/tech-talk-hardware-securitys-hi erarchy-of-attacks.html SUMMARY:Galois Tech Talk: Hardware Security's Hierarchy of Attacks LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130530T173234Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130604T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130604T103000 DTSTAMP;VALUE=DATE-TIME:20130530T173234Z LAST-MODIFIED;VALUE=DATE-TIME:20130530T173234Z UID:http://calagator.org/events/1250464319 DESCRIPTION:Five students in PSU’s Electrical and Computer Engineering Se nior Capstone sequence want to show you what they’ve created: an inexpen sive computer vision system for a quadcopter running on a Raspberry Pi b oard. One might be surprised how simple it is to code a decent object tr acking algorithm using open-source software\, and how difficult it is to keep a quadcopter from crashing into the wall in the debug stage. This talk should appeal to the RC hobbyist\, the embedded systems programmer\ , and anyone interested in the art of computer vision. The presentation will include video footage of what these students have accomplished and how they pulled it off.\n\nTags: galois\, tech talk\, quad-copter\, embe dded programming\n\nImported from: http://calagator.org/events/125046431 9 URL:http://corp.galois.com/blog/2013/5/30/tech-talk-pi-in-the-sky-how-com puter-vision-can-give-a-quadc.html SUMMARY:Pi in the Sky: How Computer Vision can give a Quadcopter Autonomo us Flight 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:20130617T185930Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130625T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130625T103000 DTSTAMP;VALUE=DATE-TIME:20130617T185930Z LAST-MODIFIED;VALUE=DATE-TIME:20130617T190230Z UID:http://calagator.org/events/1250464400 DESCRIPTION:Presented by Neil Sculthorpe. \;\n \;\nIn Haskell\, the re are many data types that would form monads were it not for the presen ce of type-class constraints on the operations on that data type. This i s a frustrating problem in practice\, because there is a considerable am ount of support and infrastructure for monads that these data types cann ot use. This talk will demonstrate that a monadic computation can be res tructured into a normal form such that the standard monad class can be u sed. The technique is not specific to monads --- it can also be applied to other structures\, such as applicative functors. One significant use case for this technique is Domain Specific Languages\, where it is often desirable to compile a deep embedding of a computation to some other la nguage\, which requires restricting the types that can appear in that co mputation.\n\nTags: galois\, functional programming\, haskell\, tech tal k\, monads\n\nImported from: http://calagator.org/events/1250464400 URL:http://corp.galois.com/blog/2013/6/17/tech-talk-the-constrained-monad -problem.html SUMMARY:Galois Tech Talk: The Constrained-Monad Problem LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130627T162721Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130702T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130702T103000 DTSTAMP;VALUE=DATE-TIME:20130627T162721Z LAST-MODIFIED;VALUE=DATE-TIME:20130627T162721Z UID:http://calagator.org/events/1250464477 DESCRIPTION:Presented by Pat Hickey. \;\n \;\nAt Galois\, we're bui lding critical flight control software using new software methods for em bedded systems programming. We will show how we used new domain-specific languages which permit low-level hardware manipulation while still prov iding guarantees of type and memory safety. The flagship application for these new languages is called SMACCMPilot\, a clean slate design of qua dcopter flight control software built on open-source hardware. This talk will introduce our new software methods and show how we built SMACCMPil ot to be high assurance without sacrificing programmer productivity.\n\n Tags: galois\, functional programming\, tech talk\, quad-copter\, embedd ed programming\n\nImported from: http://calagator.org/events/1250464477 URL:http://corp.galois.com/blog/2013/6/27/tech-talk-smaccmpilot-flying-qu adcopters-using-new-technique.html SUMMARY:Galois tech talk: SMACCMPilot: flying quadcopters using new techn iques for embedded programming LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130715T224212Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130716T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130716T103000 DTSTAMP;VALUE=DATE-TIME:20130715T224212Z LAST-MODIFIED;VALUE=DATE-TIME:20130715T224212Z UID:http://calagator.org/events/1250464562 DESCRIPTION:Presented by Jesse Hallett. \;\n \;\nTake control of yo ur hardware by installing an open build of Android. Get root access and extend the life of your device. Learn about what is involved in install ing a third-party OS on your phone or tablet.\n\nTags: galois\, android\ , tech talk\n\nImported from: http://calagator.org/events/1250464562 SUMMARY:Galois Tech Talk: Mod your Android LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130723T201833Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130729T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130729T103000 DTSTAMP;VALUE=DATE-TIME:20130723T201833Z LAST-MODIFIED;VALUE=DATE-TIME:20130723T201833Z UID:http://calagator.org/events/1250464598 DESCRIPTION:Academic papers often describe typed calculi\, but it is rare to find one in a production compiler. Indeed\, I think the Glasgow Hask ell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly statically-typed intermediate language\, inf ormally called "\;Core"\;\, or (when writing academic papers) th e more respectable-sounding "\;System FC"\;. \;\n \;\nAs r eal compilers go\, GHC's Core language is tiny: it is a slight extension of System F\, with letrec\, data types\, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core\, namely typed (but era sable) coercions that witness type equalities\, which turn Core into a p articular kind of proof-carrying code. This single addition has opened t he door to a range of source-language extensions\, such as GADTs and typ e families. \;\n \;\nIn this talk I'll describe Core\, and how it has affected GHC's development over the last two decades\, concentrating particularly on recent developments\, coercions\, evidence\, and type f amilies. \;\nTo test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a non-terminating rewrite system with non-left-linear rules.\n\nTags: galois\, haskell\, t ech talk\, compilers\, type systems\n\nImported from: http://calagator.o rg/events/1250464598 URL:http://corp.galois.com/blog/2013/7/23/tech-talk-type-directed-compila tion-in-the-wild-haskell-and.html SUMMARY:Galois tech talk: Type-directed compilation in the wild: Haskell and Core LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130909T162138Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130912T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130912T103000 DTSTAMP;VALUE=DATE-TIME:20130909T162138Z LAST-MODIFIED;VALUE=DATE-TIME:20130909T162138Z UID:http://calagator.org/events/1250464853 DESCRIPTION:Presented by Alex Groce. \;\n \;\nOne of the most effec tive ways to test complex language implementations\, file systems\, and other critical systems software is random test generation. This talk wil l cover a number of recent results that show how---despite the importanc e of hand-tooled random test generators for complex testing targets--- t here are methods that can be easily applied in almost any setting to gre atly improve the effectiveness of random testing. Surprisingly\, giving up on potentially finding any bug with every test makes it possible to f ind more bugs over all. The practical problem of finding distinct bugs i n a large set of randomly generated tests\, where the frequency of some bugs may be orders of magnitude higher than other bugs\, is also open to non ad-hoc methods. \;\n\n\nTags: galois\, testing\, tech talk\n\nIm ported from: http://calagator.org/events/1250464853 URL:http://corp.galois.com/blog/2013/9/9/tech-talk-new-directions-in-rand om-testing-from-mars-rovers.html SUMMARY:(Galois Tech Talk) New Directions in Random Testing: from Mars Ro vers to JavaScript Engines LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130912T220631Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130920T150000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130920T140000 DTSTAMP;VALUE=DATE-TIME:20130912T220631Z LAST-MODIFIED;VALUE=DATE-TIME:20130912T220631Z UID:http://calagator.org/events/1250464875 DESCRIPTION:Small unmanned aircraft---more often called drones---are set to make a big impact on agriculture. You already know about military dro nes operating overseas\, and perhaps you've even seen recreational drone s starring in youtube videos\, but as the FAA begins permitting commerci al use of unmanned aircraft in 2015\, you'll see drones replacing all so rts of roles that used to require a manned aircraft\, and taking on new roles made possible by their low cost\, versatility\, and safety. \;\ n \;\nChris Anderson will speak about the upcoming role of drones in agriculture\, a field Chris says "\;is a big data problem without th e big data."\; Chris will describe how farmers can will drones to cu rb plant disease\, conserve water\, and reduce pesticide and fertilizer use. He'll discuss the challenges ahead to integrate air vehicle systems with sensors\, specialized cameras\, and data processing.\n\nTags: galo is\, agriculture\, tech talk\, drones\n\nImported from: http://calagator .org/events/1250464875 URL:http://corp.galois.com/blog/2013/9/12/tech-talk-chris-anderson-on-usi ng-drones-in-agriculture.html SUMMARY:Galois Tech Talk: Chris Anderson on Using Drones in Agriculture LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20131018T055000Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20131022T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20131022T103000 DTSTAMP;VALUE=DATE-TIME:20131018T055000Z LAST-MODIFIED;VALUE=DATE-TIME:20131018T055000Z UID:http://calagator.org/events/1250465073 DESCRIPTION:presented by: Ashe Dryden \;\n \;\nabstract: It's been scientifically proven that more diverse communities and workplaces creat e better products and the solutions to difficult problems are more compl ete and diverse themselves. Companies are struggling to find adequate ta lent. So why do we see so few women\, people of color\, and LGBTQ people at our events and on the about pages of our websites? Even more curious ly\, why do 60% of women leave the tech industry within 10 years? Why ar e fewer women choosing to pursue computer science and related degrees th an ever before? Why have stories of active discouragement\, dismissal\, harassment\, or worse become regular news? \;\n \;\nIn this talk w e’ll examine the causes behind the lack of diversity in our communities\ , events\, and workplaces. We’ll discuss what we can do as community mem bers\, event organizers\, and co-workers to not only combat this problem \, but to encourage positive change by contributing to an atmosphere of inclusivity. \;\n \;\nbio: Ashe Dryden is an indie ruby developer living in Madison\, WI. She's been involved with the web in some form or another over the course of the past 12 years. Ashe is an outspoken educ ator for diversity\, inclusiveness\, and empathy. She's currently writin g a book on increasing diversity within companies\, as well as working o n a video series and site to serve as a resource to people who want to g et involved. When she isn't discussing technology or it’s intersection w ith culture\, she's cycling\, tweeting\, playing board games\, debating the social implications of Star Trek episodes\, being that awkward girl at the party\, and waiting for her next burrito fix.\n\nTags: galois\, c ommunity\, diversity\, inclusiveness\, women in tech\n\nImported from: h ttp://calagator.org/events/1250465073 URL:http://corp.galois.com/blog/2013/10/17/tech-talk-programming-diversit y.html SUMMARY:Galois Tech Talk: Programming Diversity LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140220T174107Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140317T190000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140317T180000 DTSTAMP;VALUE=DATE-TIME:20140220T174107Z LAST-MODIFIED;VALUE=DATE-TIME:20140310T214558Z UID:http://calagator.org/events/1250465716 DESCRIPTION:This event is free\, but please RSVP on Eventbrite (will be l inked above) \;\n \;\nEvent Description \;\nIntroducing TA3M Dr ink and Draw! We are planning a fun hands-on meetup. You will get to wor k with a team to discuss privacy\, security\, anti-surveillance\, and an ti-censorship topics and communicate your ideas through doodling! Each d iscussion group will work together to create a hand-drawn poster related to TA3M topics. This is a time to network with other individuals intere sted in these topics\, and provides a fun way to express your ideas and concerns. We will do our very best to make sure beverages of all sorts ( alcoholic and not) are available to get those creative juices flowing. & #13\;\n \;\nAfter the Drink and Draw session\, we invite attendees to join us for social time at a nearby bar/restaurant. \;\n \;\nHav e a preference about what you want to learn? Want to lead a group in tea ching a method? Email us a community@privly.org and we'll add you to the agenda. \;\n \;\nWhat is it? \;\nThis is the Techno-Activism 3rd Monday event for Portland\, Oregon! Read more about techno-activism 3rd mondays. \;\n \;\n Who should come? \;\nAnyone interested in techno-activism. We invite coders\, geeks\, artists\, and anyone else . No technical experience required. \;\n \;\nWho's hosting? \;\ nThe Privly Foundation organizes the event. Galois is generously providi ng space for the event. \;\n \;\nCode of Conduct \;\nPlease re view our code of conduct before attending the event to ensure a safe and welcoming time for all. \;\n \;\nPDXTech4Good \;\nIf you're in terested in this event\, you might also be interested in the PDXTech4Goo d meetup. \n\nTags: security\, technology\, meetup\, activism\, privacy\ , techno-activism\n\nImported from: http://calagator.org/events/12504657 16 URL:http://ta3m-pdx-9.eventbrite.com/ [TBA] SUMMARY:Portland's Techno-Activism 3rd Monday LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:6 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140327T171232Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140401T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140401T110000 DTSTAMP;VALUE=DATE-TIME:20140327T171232Z LAST-MODIFIED;VALUE=DATE-TIME:20140327T171232Z UID:http://calagator.org/events/1250465933 DESCRIPTION:Presented by John Launchbury. \;\n \;\nIn secure comput ation\, one or more parties collaborate to compute a result while keepin g all the inputs private. That is\, no-one can gain knowledge about the inputs from the other parties\, except what can be determined from the o utput of the computation. Methods of secure computation include fully ho momorphic encryption (where one party owns the input data and the other party performs the whole computation)\, and secure multiparty computatio n (where multiple parties collaborate in the computation itself). The un derlying methods are still exceedingly costly in time\, space\, and comm unication requirements\, but there are also many other practical problem s to be solved before secure computation can be usable. For programmers\ , the algorithm construction is often nonintuitive\; for compiler writer s\, the machine assumptions are very different from usual\; and for appl ication designers\, the application information flow has to match the se curity architecture. In this talk we will highlight these challenges\, a nd indicate promising research directions.\n\nTags: Galois tech talk\, c ryptography\, programming\, security\n\nImported from: http://calagator. org/events/1250465933 URL:http://corp.galois.com/blog/2014/3/27/tech-talk-practical-challenges- to-secure-computation.html SUMMARY:Galois tech talk: Practical Challenges to Secure Computation LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140402T212335Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140408T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140408T110000 DTSTAMP;VALUE=DATE-TIME:20140402T212335Z LAST-MODIFIED;VALUE=DATE-TIME:20160611T125434Z UID:http://calagator.org/events/1250465952 DESCRIPTION:Presented by Morgan Miller. \;\n \;\nCryptographic tool s have become more powerful in the last three decades. With that power h as come complexity. To use or even understand most security tools you ne ed a thorough understanding of mathematics which makes them inaccessible to the general public. The discipline of usability has been growing as well in the past three decades. There have been few but promising overla ps in usability and security which may provide vital tools for managing our digital selves\, upholding the principal of privacy\, and preserving freedom of speech.\n\nTags: Galois tech talk\, cryptography\, security\ , usability\n\nImported from: http://calagator.org/events/1250465952 URL:http://corp.galois.com/blog/2014/4/2/tech-talk-a-short-examination-on -the-intersection-of-securit.html SUMMARY:Galois tech talk LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:3 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140417T231443Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140425T110000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140425T100000 DTSTAMP;VALUE=DATE-TIME:20140417T231443Z LAST-MODIFIED;VALUE=DATE-TIME:20140417T231443Z UID:http://calagator.org/events/1250466038 DESCRIPTION:abstract: What if you want to store encrypted files on an unt rusted Cloud Server in such a way that Server does not even know if you are editing the same file today as you were yesterday\, or anything else about your usage patterns other than total amount of traffic to the Ser ver? Clearly\, no matter how strong of an encryption you use\, access pa ttern is revealed: Cloud Server can simply track where on the hard drive you read/write from – clearly encryption does not hide that information . One naive solution to prevent revealing access pattern to the Server i s to simply read all your data back from the Server and re-write your en tire data back to Server in its entirety for each read/write. This works \, but it is clearly impractical. Oblivious Random Access Memory (ORAM) is an algorithm that allows you to completely hide arbitrary access patt ern in an efficient manner. In this talk\, I will describe Oblivious RAM from the ground up\, starting from my own Ph.D. thesis work on this top ic (STOC 1990\, MIT Ph.D. 1992) which showed the first efficient ORAM. T he Journal Version of this work gained over 450 references according to Google Scholar [Ostrovsky-Goldreich JACM 1996] and ORAM became an import ant area of research in Cryptography in the last 5 years. I will describ e surprising connections of ORAM to (1) tamper-proof embedded systems\, (2) Software Protection (3) Secure Multi-Party and Secure Two Party Comp utation as well as (4) ways to securely compile programs with loops\, “g oto” statements\, recursion\, etc. into Garbled programs without “unroll ing” the execution path\, yet not revealing anything about the execution path. I will also compare and contrast ORAM to Single-Server Private In formation Retrieval (Single-server PIR)\, which I co-invented with Kushi levitz in 1997\, and explain important differences of these two models. The talk will be self-contained and accessible to the general audience.& #13\;\n \;\nSpeaker bio: Rafail Ostrovsky is a Professor of Computer Science and Professor of Mathematics at UCLA and co-founder of Stealth S oftware Technologies\, Inc. He has over 200 papers published in refereed journals and conferences and has 11 U.S. Patents issued. In 2013\, Dr. Ostrovsky was inducted as an IACR (International Association of Cryptolo gic Research) Fellow. He currently serves as Vice-Chair of the IEEE Tech nical Committee on Mathematical Foundations of Computing and has served on 38 international conference Program Committees including serving as a PC chair of FOCS 2011. He is a member of the Editorial Board of JACM\, the Editorial Board of Algorithmica\; and the Editorial Board of Journal of Cryptology\; he serves on the Editorial and Advisory Board of the In ternational Journal of Information and Computer Security and is a member of the steering committee of the international symposium of Security in Communication Networks (SCN). He is a recipient of multiple academic aw ards and honors and has google h-index factor of 55. At UCLA\, Prof. Ost rovsky heads security and cryptography multi-disciplinary Research Cente r (http://www.cs.ucla.edu/security/) at Henry Samueli School of Engineer ing and Applied Science.\n\nTags: Galois tech talk\, cryptography\, secu rity\, privacy\n\nImported from: http://calagator.org/events/1250466038 URL:http://corp.galois.com/blog/2014/4/17/tech-talk-a-gentle-introduction -to-hiding-usage-patterns.html SUMMARY:Galois tech talk: A Gentle Introduction to Hiding Usage Patterns LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140501T044348Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140507T193000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140507T173000 DTSTAMP;VALUE=DATE-TIME:20140501T044348Z LAST-MODIFIED;VALUE=DATE-TIME:20140502T041814Z UID:http://calagator.org/events/1250466105 DESCRIPTION:RSVP on the meetup.com site. Please and thank you! \;\n 3\;\nBe at the door by 5:30pm. \;\n \;\nMessage me on Skype: tyler zika if you are running behind so we can buzz you in. \;\n \;\nSma ll presentation on the meetup idea and values at 5:45pm by Tyler Zika.&# 13\;\n \;\nSocialize\, forming Master Mind groups\, coding\, and brai nstorming from 6-7pm. \;\n \;\nAnother small presentation. Topic a nd speaker TBA for remainder of meetup. \;\n \;\nHappy Coding!\n\ nTags: programming\, pair programming\, web development\, computer scien ce\, ruby\, python\, javascript\, beginners\, education\, social\, open source\, meetup\n\nImported from: http://calagator.org/events/1250466105 URL:http://www.meetup.com/Portland-Novice-Programmers/ SUMMARY:Portland Novice Programmers Meetup (First One!) LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:4 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140602T201932Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140605T153000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140605T143000 DTSTAMP;VALUE=DATE-TIME:20140602T201932Z LAST-MODIFIED;VALUE=DATE-TIME:20140602T201932Z UID:http://calagator.org/events/1250466378 DESCRIPTION:Correct-By-Construction Control Synthesis in Model-Based Desi gn of Autonomous Systems \;\n \;\nspeaker: \;\nUfuk Topcu \; \n \;\nabstract: How can we affordably build trustworthy autonomous\, networked systems? Partly motivated by this question\, I describe a shi ft from the traditional "\;design+verify"\; approach to "\;s pecify+synthesize"\; in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction\, hiera rchical control protocols. These results account for hybrid dynamics tha t are subject to rich temporal logic specifications and heterogenous unc ertainties\, and that operate in adversarial environments. They combine ideas from control theory with those from computer science\, and exploit underlying system-theoretic interpretations to suppress the inherent co mputational complexity. The expressivity of the resulting design methodo logy enables us to formally investigate a number of emerging issues in a utonomous\, networked systems. I conclude my talk with a brief overview of several such issues from my ongoing projects: (i) compositional synth esis for the so-called fractionated systems\; (ii) effects of perception imperfections on protocol synthesis\; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctnes s\; and (iv) human-embedded autonomy. \;\n \;\nbio: Ufuk Topcu is a Research Assistant Professor in the Department of Electrical and Syste ms Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California\, Berkeley and was a Postdoctoral Scho lar at the California Institute of Technology until 2012. His research i s on the analysis\, design\, and verification of autonomous\, networked systems.\n\nTags: Galois tech talk\, control systems\, verification\, au tonomous systems\n\nImported from: http://calagator.org/events/125046637 8 URL:http://corp.galois.com/blog/2014/6/2/tech-talk-correct-by-constructio n-control-synthesis-in-model.html SUMMARY:Galois tech talk: Correct-By-Construction Control Synthesis in Mo del-Based Design of Autonomous Systems LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140602T203008Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140606T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140606T110000 DTSTAMP;VALUE=DATE-TIME:20140602T203008Z LAST-MODIFIED;VALUE=DATE-TIME:20140602T203008Z UID:http://calagator.org/events/1250466379 DESCRIPTION:Formal Verification of Cyber-Physical Systems \;\n \;\n speaker: \;\nPavithra Prabhakar \;\n \;\nabstract: Cyber-Physic al Systems (CPS) refer to systems in which control\, computation and com munication converge to achieve complex functionalities. The ubiquitous d eployment of cyber-physical systems in safety critical applications incl uding aeronautics\, automotive\, medical devices and industrial process control\, has pressurized the need for the development of automated anal ysis methods to aid the design of high-confidence systems. The talk will focus on an important feature of cyber-physical systems\, namely\, the mixed discrete-continuous behaviors manifesting as a result of the inter action of a network of embedded processors with the physical world. Hybr id Automata are a popular formalism for modeling systems exhibiting both discrete and continuous behaviors. We discuss formal approaches for the verification of hybrid automata. More precisely\, scalable approaches b ased on approximations\, including predicate abstraction\, counter-examp le guided abstraction refinement and bounded error approximations\, will be discussed in the context of safety and stability analysis. We will p resent applications of the techniques on hybrid automata models. \;\n \;\nbio: Pavithra Prabhakar is on the faculty at the IMDEA Software Institute in Madrid\, Spain\, since 2011. Previously\, she obtained her doctorate in Computer Science from the University of Illinois at Urbana- Champaign\, from where she also obtained a masters in Applied Mathematic s. She has a masters degree in Computer Science from the Indian Institut e of Science\, Bangalore and a bachelors degree from the National Instit ute of Technology\, Warangal\, in India. She spent the year between 2011 -2012 at the California Institute of Technology as a CMI (Center for Mat hematics of Information) fellow. Her main research interest is in Formal Analysis of Cyber-Physical Systems\, more precisely\, hybrid systems\, with focus on both theoretical and practical aspects.\n\nTags: Galois te ch talk\, verification\, cyber-physical systems\n\nImported from: http:/ /calagator.org/events/1250466379 URL:http://corp.galois.com/blog/2014/6/2/tech-talk-formal-verification-of -cyber-physical-systems.html SUMMARY:Galois tech talk: Formal Verification of Cyber-Physical Systems LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140522T164018Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140611T193000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140611T173000 DTSTAMP;VALUE=DATE-TIME:20140522T164018Z LAST-MODIFIED;VALUE=DATE-TIME:20140522T164051Z UID:http://calagator.org/events/1250466287 DESCRIPTION:Small presentation on the Meetup idea and values at 5:45pm by Tyler Zika. \;\n \;\nSocializing\, forming Master Mind groups\, c oding\, and brainstorming from 6-7pm. Bring your laptop if you want to s how what you are working on or you'd like some help. \;\n \;\nAnot her small presentation. Topic and speaker TBA for remainder of Meetup. & #13\;\n \;\nRSVP on meetup.com site. Please and thank you. \;\n 3\;\nHappy Coding! \n\nTags: meetup\, programming\, galois\n\nImported f rom: http://calagator.org/events/1250466287 URL:http://www.meetup.com/Portland-Novice-Programmers/ SUMMARY:Portland Novice Programmers Monthly Meetup LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140609T214110Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140613T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140613T110000 DTSTAMP;VALUE=DATE-TIME:20140609T214110Z LAST-MODIFIED;VALUE=DATE-TIME:20140609T214110Z UID:http://calagator.org/events/1250466415 DESCRIPTION:speaker: Joachim Breitner \;\n \;\nabstract: We will ta ke you on a guided tour through the memory of a running Haskell program and get to peek at the raw bytes of Haskell values. We’ll see how unifor mity allows for polymorphic functions and data structures\, where the ga rbage collector finds the information it needs and learn to predict how large certain values tend to become. With the help of a visualization to ol (ghc-vis) we will also see laziness and sharing at work\, and reveal the mystery of how Haskell fits infinite data structures into a finite a mount of memory. \;\n \;\nbio: Joachim Breitner is a PhD student a t the Karlsruhe Institute of Technology\, Germany\, where he works on th e semantics of lazy functional programming language and on interactive t heorem provers. He maintains the Haskell packages for Debian and Ubuntu and contributes to GHC. When he is AFK\, he enjoys board games\, swing d ancing\, softball and paragliding.\n\nTags: Galois tech talk\, haskell\, visualization\, runtime\n\nImported from: http://calagator.org/events/1 250466415 URL:http://corp.galois.com/blog/2014/6/9/tech-talk-haskell-bytes.html SUMMARY:Galois tech talk: Haskell Bytes LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140610T004507Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140630T193000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140630T173000 DTSTAMP;VALUE=DATE-TIME:20140610T004507Z LAST-MODIFIED;VALUE=DATE-TIME:20140613T192752Z UID:http://calagator.org/events/1250466419 DESCRIPTION:(from the Meetup page\, please RSVP there!) \;\n \;\nOu r inaugural meeting will be a full-fledged office hours session! Bring y our projects\, or just your excitement for learning. \;\n \;\nWe w ill also be taking feedback on the format of the meetup\, the scheduling \, and anything else that will help make this a valuable resource for yo u. If you are not able to attend\, let us know if there's anything we ca n do to help make it work in the future.\n\nTags: haskell\, functional p rogramming\, peer mentoring\n\nImported from: http://calagator.org/event s/1250466419 URL:http://www.meetup.com/Portland-Haskell-Office-Hours/events/188165452/ SUMMARY:Haskell Office Hours LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140707T185453Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140708T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140708T110000 DTSTAMP;VALUE=DATE-TIME:20140707T185453Z LAST-MODIFIED;VALUE=DATE-TIME:20140707T185453Z UID:http://calagator.org/events/1250466607 DESCRIPTION:abstract: Sunroof is an embedded Haskell Domain Specific Lang uage (DSL) that compiles to JavaScript. Blank Canvas is an embedded Hask ell DSL that provides direct access to the HTML5 JavaScript Canvas. Both DSLs superficially provide the same capabilities\, but make different t rade-offs in the DSL design space. Sunroof uses monadic reification to e nable bindings in the DSL to be translated into bindings in JavaScript\, while blank canvas has every binding make a round trip from Haskell\, t o JavaScript\, back to Haskell. In this talk\, we will present the speci fics of both DSLs\, using examples\, then use both DSLs to outline the d ifference choices available when designing and implementing embedded DSL s in Haskell. \;\n \;\nbio: Andrew (Andy) Gill was born and educat ed in Scotland\, and has spent his professional career in the United Sta tes\, working both in industry\, and academia. Andy received his Ph.D. f rom the University of Glasgow in 1996\, then spent three years in indust ry as a compiler developer\, and a year in academia as a principal proje ct scientist. He co-founded Galois in 2000\, a technology transfer compa ny that used language technologies to create trustworthiness in critical systems. In 2008\, he joined the University of Kansas\, and in 2014 he was a recipient of the NSF CAREER Award. \;\n \;\nAndy believes th at functional languages like Haskell are a great medium for expressing a lgorithms and solving problems. Since returning to academia\, he has tar geted the application areas of telemetry and signal processing\, special izing in generating high performance circuits from specifications. His r esearch interests include optimization\, language design\, debugging\, a nd dependability. The long-term goal of his research is to offer enginee rs and practitioners the opportunity to write clear and high-level execu table specifications that can realistically be compiled into efficient i mplementations.\n\nTags: Galois tech talk\, haskell\, DSL\, javascript\n \nImported from: http://calagator.org/events/1250466607 URL:http://corp.galois.com/blog/2014/7/7/tech-talk-sunroof-and-a-blank-ca nvas-a-tail-of-two-dsls.html SUMMARY:Galois tech talk: Sunroof and a Blank Canvas: A tail of two DSLs LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140728T185801Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140801T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140801T110000 DTSTAMP;VALUE=DATE-TIME:20140728T185801Z LAST-MODIFIED;VALUE=DATE-TIME:20140728T185801Z UID:http://calagator.org/events/1250466723 DESCRIPTION:Abstract: \;\nRecords in Haskell are notoriously difficult to compose\; many solutions have been proposed. Vinyl lies in the space of library-level approaches\, and addresses polymorphism\, extensibilit y\, effects and strictness. I describe how Vinyl approaches record famil ies over arbitrary key spaces using a Tarski universe construction\, as well as a method for immersing each field of a record in a chosen effect modality. Moreover\, I give a characterization of records as sheaves of types\, which provides a clear motivation for the safety of subtyping a nd coercion of records\, and a path toward records with non-trivial topo logies on their key spaces. Lastly\, I describe an interpretation of Vin yl-style records into Type Theory as finite products over containers\, l eading to many possible and interesting extensions\, such as composition al universes of polymorphic variants\, as well as inductive and coinduct ive types. \;\n \;\nBio: \;\nI'm an amateur type theorist who s tudied Historical Linguistics during my undergraduate at UC Berkeley\, s pecializing in Ancient Greek\, Sumerian\, Akkadian and Anglo-Saxon. I'm particularly interested in type-theoretic syntax and semantics for natur al language\, and am presently exploring the use of multi-modal combinat ory categorial grammar for interpreting the hyperbaton-rich syntax of an cient Indo-European languages. In addition to my interest in linguistics \, I have become obsessed with extensionality\, realizability and PER se mantics for Martin-Löf Type Theory\, and am currently trying to come up with an extension to Observational Type Theory which internalizes furthe r extensional concepts\, such as union\, intersection\, image and PER ty pes whilst retaining decidability of type checking. \;\n\n\nTags: Gal ois tech talk\n\nImported from: http://calagator.org/events/1250466723 URL:http://galois.com/blog/2014/07/tech-talk-vinyl-records-haskell-type-t heory/ SUMMARY:Galois tech talk: Vinyl: Records in Haskell & Type Theory LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140729T160522Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140808T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140808T110000 DTSTAMP;VALUE=DATE-TIME:20140729T160522Z LAST-MODIFIED;VALUE=DATE-TIME:20140729T160522Z UID:http://calagator.org/events/1250466729 DESCRIPTION:**abstract:** C programs are notoriously difficult to reason about\, either for safety or full functional correctness. Even with a pr ogram logic powerful enough to prove the necessary properties\, the proo f has the assumption that the compiler behaves exactly the way it is exp ected to. Verified Software Toolchain (VST) answers this problem by prov iding a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational sema ntics of C\, the same operational semantics compiled by the proved-corre ct CompCert verified optimizing C compiler. Both of those proofs are mac hine-checked in Coq\, an interactive proof assistant. This talk will pre sent the basics of VST\, followed by an example proof of a C program. 3\;\n \;\n**bio:** Josiah (Joey) Dodds is an intern at Galois for the summer\, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton\, where he has been verifying information-flow properties and C programs in Coq.\n\nTa gs: Galois tech talk\n\nImported from: http://calagator.org/events/12504 66729 URL:http://galois.com/blog/2014/07/tech-talk-verifying-c-programs-coq-usi ng-vst/ SUMMARY:Galois tech talk: Verifying C programs in Coq using VST LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140922T214016Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140923T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140923T110000 DTSTAMP;VALUE=DATE-TIME:20140922T214016Z LAST-MODIFIED;VALUE=DATE-TIME:20140922T214016Z UID:http://calagator.org/events/1250467025 DESCRIPTION:abstract: Automatic device driver synthesis is a radical appr oach to creating drivers faster and with fewer defects by generating the m automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit\, called Termite-2. Termite-2 is the first tool to combine the power of automati on with the flexibility of conventional development. It is also the firs t practical synthesis tool based on abstraction refinement. Finally\, it is the first synthesis tool to support automated debugging of input spe cifications. I will explain the main principles behind the tool and give a brief demo of its capabilities. \;\n \;\nbio: Leonid Ryzhyk is a postdoctoral fellow at the University of Toronto and a researcher at N ICTA. He received his PhD from the University of New South Wales in 2010 .\n\nTags: Galois tech talk\n\nImported from: http://calagator.org/event s/1250467025 URL:http://galois.com/blog/2014/09/tech-talk-automatic-device-driver-synt hesis/ SUMMARY:Galois tech talk: Automatic Device Driver Synthesis LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20141013T202114Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141021T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141021T110000 DTSTAMP;VALUE=DATE-TIME:20141013T202114Z LAST-MODIFIED;VALUE=DATE-TIME:20141013T202114Z UID:http://calagator.org/events/1250467156 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are open to the interested public–please join us! (There is no need to pre-register for the talk.) \;\n \;\nabstract: \;\nAt this yea r’s WWDC\, Apple announced Swift\, a new programming language for iOS an d OS X development. In this talk\, I’d like to give a brief overview of the language\, focussing on its ‘functional features’. I’ll try to demon strate that there are exciting new possibilities for applying functional programming technology to a new platform — like writing an app that com putes Fibonacci numbers without using a for-loop. \;\n \;\nbio: 3\;\nWouter Swierstra is a lecturer at the University of Utrecht. He has recently written a book\, Functional Programming in Swift\, together wi th Chris Eidhof and Florian Kugler.\n\nTags: Galois tech talk\, function al programming\, swift\n\nImported from: http://calagator.org/events/125 0467156 URL:http://galois.com/blog/2014/10/tech-talk-functional-programming-swift / SUMMARY:Galois tech talk: Functional programming in Swift LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20141020T232833Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141024T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20141024T110000 DTSTAMP;VALUE=DATE-TIME:20141020T232833Z LAST-MODIFIED;VALUE=DATE-TIME:20141020T232833Z UID:http://calagator.org/events/1250467198 DESCRIPTION:abstract: \;\nWe present four calculi for gradual typing: $\\lambda\\B$\, based on the blame calculus of Wadler and Findler~(2009) \; $\\lambda\\C$\, based on the coercion calculus of Henglein~(1994)\; a nd $\\lambda\\T$ and $\\lambda\\W$\, based on the threesome calculi with and without blame of Siek and Wadler~(2010). We define translations fro m $\\lambda\\B$ to $\\lambda\\C$\, from $\\lambda\\C$ to $\\lambda\\T$\, and from $\\lambda\\T$ to $\\lambda\\W$. We show each of the translatio ns is fully abstract —far stronger correctness results than have previou sly appeared. \;\n \;\nbio: \;\nPhilip Wadler is Professor of T heoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh\, past chair of A CM SIGPLAN\, past holder of a Royal Society-Wolfson Research Merit Fello wship\, and a winner of the POPL Most Influential Paper Award. Previousl y\, he worked or studied at Stanford\, Xerox Parc\, CMU\, Oxford\, Chalm ers\, Glasgow\, Bell Labs\, and Avaya Labs\, and visited as a guest prof essor in Copenhagen\, Sydney\, and Paris. He has an h-index of 60\, with more than 18\,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell\, Java\, and XQuery\, and is a co -author of Introduction to Functional Programming (Prentice Hall\, 1988) \, XQuery from the Experts (Addison Wesley\, 2004) and Generics and Coll ections in Java (O’Reilly\, 2006). He has delivered invited talks in loc ations ranging from Aizu to Zurich.\n\nTags: Galois tech talk\, type the ory\, lambda calculus\n\nImported from: http://calagator.org/events/1250 467198 URL:https://galois.com/blog/2014/10/tech-talk-by-philip-wadler/ SUMMARY:Galois tech talk by Philip Wadler LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20150608T183821Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150616T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150616T110000 DTSTAMP;VALUE=DATE-TIME:20150608T183821Z LAST-MODIFIED;VALUE=DATE-TIME:20150608T183821Z UID:http://calagator.org/events/1250468602 DESCRIPTION:abstract: \;\nIn this talk\, I’ll give an introduction to differential privacy with an emphasis on its relationship to machine lea rning\, and its usefulness outside of privacy. Along the way\, I’ll give a taste for the mathematical tools that can be used to achieve differen tial privacy. My thesis is that anyone who cares about data should care about the tools that the differential privacy literature offers. \;\n \;\nbio: \;\nKatrina Ligett is an assistant professor of computer science and economics at Caltech. Before joining Caltech in 2011\, she did postdoctoral work at Cornell\, and she received her PhD in computer science from Carnegie Mellon in 2009. Her primary research interests are in mathematical foundations for data privacy\, and in game theory. She has received an NSF Career Award\, a Microsoft Research Faculty Fellowsh ip\, a Google Faculty Research Award\, and an Okawa Foundation Research Grant.\n\nTags: Galois tech talk\, privacy\n\nImported from: http://cala gator.org/events/1250468602 URL:http://galois.com/blog/2015/06/tech-talk-differential-privacy-toolkit -stability-robustness-statistical-validity/ SUMMARY:Galois tech talk: Differential Privacy – A Toolkit for Stability\ , Robustness\, and Statistical Validity LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20150608T184122Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150618T110000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150618T100000 DTSTAMP;VALUE=DATE-TIME:20150608T184122Z LAST-MODIFIED;VALUE=DATE-TIME:20150608T184122Z UID:http://calagator.org/events/1250468603 DESCRIPTION:abstract: \;\n \;\nCH2O is the PhD project of Robbert K rebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fu ndamentally inconsistent. \;\n \;\nThere are three versions of the CH2O semantics: a (small step) operational semantics\, an executable se mantics\, and an axiomatic semantics (a separation logic for C). The mos t important properties — soundness and completeness results\, subject re duction and progress\, correctness of the type checker — have all been p roved. All definitions and proofs have been fully formalized in Coq\, wi thout any axioms and on top of a non-trivial support library. \;\n 3\;\nThe CH2O project has two abstract C-like languages. A significant s ubset of C called “CH2O abstract C” is translated into a simplified lang uage called “CH2O core C”. This translation is written in Coq and implic itly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C. \;\n \;\nThe executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standa lone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does no t yet support I/O (nor the exit function)\, a small hack allows the CH2O interpreter to still explore programs that call printf. \;\n \;\n The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert a nd CH2O are that the CH2O semantics has explicit typing judgments for ev erything\, and that CH2O applies to any ISO compliant compiler. \;\n& #13\;\nbio: \;\n \;\nI have a master degree in mathematics (my the sis was about conformal supergravity)\, and a PhD in computer science\, both from the University of Amsterdam. I also worked as a system adminis trator at the University of Utrecht. \;\n \;\nCurrently I’m an ass istant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using in teractive theorem provers\, but recently I have been getting interested in practical program verification\, where interactive proof is used when automation doesn’t cut it. \;\n \;\nAt the moment I am an alterna te member of WG14\, and I won a price in the IOCCC twice. And my favorit e project is the CakeML/verified-HOL Light project. \;\n\n\nTags: Gal ois tech talk\, C\, theorem proving\, semantics\n\nImported from: http:/ /calagator.org/events/1250468603 URL:http://galois.com/blog/2015/06/tech-talk-ch2o-project-making-sense-c- standard/ SUMMARY:Galois tech talk: The CH2O project: making sense of the C standar d LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20151010T003909Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20151112T193000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20151112T173000 DTSTAMP;VALUE=DATE-TIME:20151010T003909Z LAST-MODIFIED;VALUE=DATE-TIME:20151010T004020Z UID:http://calagator.org/events/1250469207 DESCRIPTION:(from the Meetup description): \;\n \;\nWelcome to Port land Haskell Office Hours! Bring your projects\, or just your excitement for learning. \;\n \;\nWe will still be taking feedback on the fo rmat of the meetup\, the scheduling\, and anything else that will help m ake this a valuable resource for you. If you are not able to attend\, le t us know if there's anything we can do to help make it work in the futu re. \;\n \;\n-- \;\n \;\nAbout Haskell Office Hours: \;\n \;\nShow up with a project you'd like to share or a problem that you 're stuck on\, and we'll learn together in small\, supportive groups! An "\;Office Hours"\; meetup is an opportunity for people of all s kill levels to come together\, learn\, and have fun. Our goal is to focu s on inclusion and active participation through teaching and mentorship. \;\n \;\nThe meetup is hosted at Galois\, which uses Haskell exte nsively in industry\, and is well-attended by Galwegians who are eager t o share their excitement for Haskell and functional programming. This gr oup is very new\, so you still have an opportunity to shape how we do th ings. If the schedule doesn't work for you\, or if we can do anything to help you feel more safe and welcome\, let us know!\n\nTags: haskell\, M entors\, meetup\n\nImported from: http://calagator.org/events/1250469207 URL:http://www.meetup.com/Portland-Haskell-Office-Hours/events/225956310/ SUMMARY:Haskell Office Hours LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:3 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20160314T224157Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160318T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160318T103000 DTSTAMP;VALUE=DATE-TIME:20160314T224157Z LAST-MODIFIED;VALUE=DATE-TIME:20160314T224157Z UID:http://calagator.org/events/1250469962 DESCRIPTION:abstract: \;\n \;\nThe Curry-Howard Isomorphism motivat es the well known proofs-as-programs interpretation. Under that interpre tation\, sufficiently different proofs yield different programs. This wo rk is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example\, we discovered that the sta ndard type bind \;\n(M a ->\; (a ->\; M b) ->\; M b) does not c ontain enough information to allow many proofs to go through. For lists\ , an implicit assumption on the function of type ( a ->\; M b) is that the input of type a is an element of the list of type M b. We developed an new typeclass of epsilon-monads to be able to strengthen the functio n type. Epsilon-monads are monads that support a membership predicate. E psilon-monads enabled the development of a bind-induction proof rule whi ch allows the extraction of monadic programs using the bind operator. Al so\, epsilon monads allow for extensional specifications of monadic prog rams. We used the Coq theorem prover to formalize the definitions and to prove many properties of the formalization. This is joint work with Had i Shafe’i. \;\n \;\nbio: \;\n \;\nJames Caldwell is Professo r and Head of the Computer Science Department at the University of Wyomi ng. He earned his PhD from Cornell in the Nuprl group advised by Robert Constable. Before moving to the University of Wyoming in 1998\, he was a researcher in the formal methods group at the NASA Langley Research cen ter. He moved to NASA from the Electric Corporate R&\;D center in Sch enectady\, NY where he was first exposed to formal verification. He has MS and BS degrees in computer science from SUNY Albany. Before coming to computer science he studied painting and sculpture at the School of the Museum of Fine Arts\, Boston. \;\n\n\nTags: Galois tech talk\, curry -howard isomorphism\, proofs\n\nImported from: http://calagator.org/even ts/1250469962 URL:http://galois.com/blog/2016/03/tech-talk-toward-extracting-monadic-pr ograms-from-proofs/ SUMMARY:Galois Tech talk: Toward Extracting Monadic Programs from Proofs 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:20170616T204045Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20170626T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20170626T103000 DTSTAMP;VALUE=DATE-TIME:20170616T204045Z LAST-MODIFIED;VALUE=DATE-TIME:20170616T204045Z UID:http://calagator.org/events/1250472092 DESCRIPTION:Abstract: \;\nRecent progress in AI and machine learning i s stimulating interest in applying AI in high stakes applications such a s self-driving cars\, surgical robots\, and autonomous weapons systems. These applications require high levels of software assurance and resilie nce\, but virtually all AI research has focused on raw performance witho ut paying attention to questions of robustness and resilience. \;\n&# 13\;\nIn this talk\, I will survey AI research that aims to create robus t systems. I will consider both robustness to “known unknowns” and robus tness to “unknown unknowns” — that is\, to unmodeled aspects of the envi ronment. \;\n \;\nOne technology that is relevant to creating robu st AI systems is anomaly detection. In the second part of the talk\, I w ill survey the work at Oregon State on anomaly detection. I’ll discuss o ur recent research on applying anomaly detection to problems of fraud de tection and equipment diagnosis and discuss methods for explaining anoma ly alarms to an analyst and incorporating analyst feedback into the anom aly detection process. \;\n \;\nBio: \;\nDr. Tom Dietterich (AB Oberlin College 1977\; MS University of Illinois 1979\; PhD Stanford Un iversity 1984) is Professor Emeritus and Director of Intelligent Systems Research in the School of Electrical Engineering and Computer Science a t Oregon State University\, where he joined the faculty in 1985. Dietter ich has devoted his career to machine learning and artificial intelligen ce. He has authored more than 180 publications and two books. His resear ch is motivated by challenging real world problems ranging from personal information \;\nmanagement\, to drug design\, to sustainability\, an d most recently to problems in safe and robust artificial intelligence. Dietterich has also devoted many years of service to the research commun ity. He is Past President of the Association for the Advancement of Arti ficial Intelligence\, and he previously served as President of AAAI (201 4-16) and as the founding president of the International Machine Learnin g Society (2001-08). Other major roles include Executive Editor of the j ournal Machine Learning (1992-98)\, co-founder of the Journal for Machin e Learning Research (2000)\, and program chair of AAAI 1990 and NIPS 200 0. He is currently the moderator for machine learning on arXiv. Dietteri ch is a Fellow of the ACM\, AAAS\, and AAAI.\n\nTags: machine learning\, Artificial Intelligence\, computer science\, anomaly detection\n\nImpor ted from: http://calagator.org/events/1250472092 URL:http://galois.com/blog/2017/06/robust-artificial-intelligence-anomaly -detection/ SUMMARY:Galois Tech Talk: Robust Artificial Intelligence and Anomaly Dete ction LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20171006T211650Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20171023T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20171023T103000 DTSTAMP;VALUE=DATE-TIME:20171006T211650Z LAST-MODIFIED;VALUE=DATE-TIME:20171006T211650Z UID:http://calagator.org/events/1250472629 DESCRIPTION:Abstract: \;\nRust is a new systems programming language t hat promises to overcome the seemingly fundamental tradeoff between high -level safety guarantees and low-level control over resource management. Unfortunately\, none of Rust’s safety claims have been formally proven\ , and there is good reason to question whether they actually hold. Speci fically\, Rust employs a strong\, ownership-based type system\, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this work\, we present RustBelt \, the first formal (and machine-checked) safety proof for a language re presenting a realistic subset of Rust. Our proof is extensible in the se nse that\, for each new Rust library that uses unsafe features\, we can say what verification condition it must satisfy in order for it to be de emed a safe extension to the language. We have carried out this verifica tion for some of the most important libraries that are used throughout t he Rust ecosystem. In the talk\, I will first review some of the essenti al features of Rust\, and then explain some of the key ideas behind the RustBelt verification. \;\n \;\nBio: \;\nDerek Dreyer is a prof essor of computer science at the Max Planck Institute for Software Syste ms (MPI-SWS)\, and recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award. His research runs the gamut from the type theory of h igh-level functional languages\, down to the verification of compilers a nd low-level concurrent programs under relaxed memory models. He is cur rently leading the RustBelt project\, which focuses on building the firs t formal foundations for the Rust programming language. He also knows a thing or two about Scotch whisky.\n\nTags: rust\, RustBelt\, computer s cience\n\nImported from: http://calagator.org/events/1250472629 URL:https://galois.com/blog/2017/10/rustbelt-securing-foundations-rust-pr ogramming-language-2/ SUMMARY:Galois Tech Talk: RustBelt: Securing the Foundations of the Rust Programming Language LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20171204T211907Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20171208T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20171208T110000 DTSTAMP;VALUE=DATE-TIME:20171204T211907Z LAST-MODIFIED;VALUE=DATE-TIME:20171204T211907Z UID:http://calagator.org/events/1250472934 DESCRIPTION:Abstract: \;\n \;\nHabit is a high-level programming la nguage\, originally based on Haskell\, that was designed to meet the nee ds of high assurance\, very low-level software development. The most re cent version of the language report was completed in 2010\, and an initi al working prototype implementation was developed by the HASP group at P SU. However\, there has not been a lot of externally visible news about the language or its implementation since then. In this talk\, I will p rovide an introduction to the goals of Habit (no previous experience is assumed)\, and an update on the status of its current implementation as we continue to edge towards a broader public release. In particular\, t his talk will discuss the challenges of meeting the performance requirem ents for typical systems software\; the benefits of programming in a sou rce language with high-level functional abstractions and expressive type s\; and the role that whole-program optimization can play in bridging be tween these two worlds. \;\n \;\nBio: \;\n \;\nMark Jones is a professor in the Department of Computer Science at Portland State Uni versity in Portland\, Oregon. His primary research focus is on the use of advanced programming language technologies that support the construct ion and certification of secure and reliable software systems. \;\n\n \nTags: computer science\, programming languages\n\nImported from: http: //calagator.org/events/1250472934 URL:https://galois.com/blog/2017/12/update-habit-programming-language/ SUMMARY:Galois Tech Talk: An Update on the Habit Programming Language LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR