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:20150308T020000 RDATE:20150308T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20150801T002013Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150812T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150812T110000 DTSTAMP;VALUE=DATE-TIME:20150801T002013Z LAST-MODIFIED;VALUE=DATE-TIME:20150801T002013Z UID:http://calagator.org/events/1250468873 DESCRIPTION:abstract: \;\n \;\nSoftware-dependent critical systems that impact daily life are rapidly increasing in number\, size\, and com plexity. Unfortunately\, inadequate software and systems engineering can lead to accidents that cause economic disaster\, injuries\, or even dea th. There is a growing reliance on development and verification tools to reduce costs\, better manage complexity\, and to increase confidence in these systems. Recent standards for critical systems have an increased emphasis on characterizing the requirements of tools used in the certifi cation context and the particular certification obligations that these t ools can discharge. In the case of avionics\, DO-333 explicitly addresse s the role/use of formal methods tools\, e.g.\, allowing formal verifica tion of code compliance to procedure contracts to complement unit testin g\, and DO-330 addresses tool qualifications. \;\n \;\nIn this tal k\, I will present the Kiasan symbolic execution framework that can be u sed to automatically check varying degrees of functional correctness pro perties of critical systems — ranging from absence of runtime errors to compositional reasoning of deep semantical contracts of complex data str uctures. One notable feature of Kiasan is the focus on explicating its a nalysis results to describe inconclusive analysis results in cases where it cannot clearly refute or verify properties. Similar to other symboli c execution tools\, Kiasan generates counter-examples or test cases as e vidence for (conclusive) contract violations. In contrast to others\, ho wever\, Kiasan can generate strong evidence for its (conclusive) verific ation results in the form of Coq proof objects. This is achieved by firs t formalizing Kiasan’s symbolic execution (abstract) semantics in Coq an d proving that it is sound and relatively complete with respect to the ( concrete) semantics of the system programming language\; this is done on ce and for all (for a particular system programming language) and establ ishes a relatively small trust base. We believe that Kiasan’s evidence-b ased trust approach can be used to help in software certifications of sa fety-critical systems as well as in tool qualification processes. \;\ n \;\nbio: \;\n \;\nRobby is a Professor in the Computing and I nformation Sciences (CIS) Department at Kansas State University. In addi tion to symbolic execution-based verification\, he works on dataflow fra mework for analyzing security vulnerability in mobile apps\, device mode ling for interoperable medical devices\, and a hazard analysis platform. In the past\, he worked on software model checking\, data/predicate abs tractions\, program dependences (slicing)\, and software specification t echniques.\n\nTags: Galois tech talk verification Coq\n\nImported from: http://calagator.org/events/1250468873 URL:http://galois.com/blog/2015/08/tech-talk-evidence-based-trust-symboli c-execution-based-verification/ SUMMARY:Galois tech talk: Evidence-based Trust of Symbolic Execution-base d Verification LOCATION:Galois Inc: 421 Sw 6th Ave Ste 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR