[Pl-seminar] Reminder: 6/1 Seminar: Cesare Tinelli, CoCoSpec: A Mode-aware Contract Language for Reactive Systems

[Daniel Patterson]

Reminder: This is next week, but it is on Thursday (not our normal
day), and at 11AM (not our normal time).

Daniel Patterson <dbp at ccs.neu.edu> writes:

> NUPRL Seminar presents
>
> Cesare Tinelli
> University of Iowa
> Host: Thomas Wahl
>
> 11AM-12:30PM (NOTE: THIS IS EARLIER THAN OUR NORMAL TIME!)
> Thursday, June 1st, 2017 (NOTE: THIS IS NOT OUR STANDARD DAY OF WEEK!)
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
>
>
> CoCoSpec: A Mode-aware Contract Language for Reactive Systems
>
> Abstract:
>
> Contract-based software development is a leading methodology for the
> construction of safety- and mission-critical embedded systems. Contracts
> are an effective way to establish boundaries between components and can
> be used efficiently to verify global properties by using compositional
> reasoning techniques. A contract specifies the assumptions a component
> makes on its context and the guarantees it provides. Requirements in the
> specification of a component are often case-based, with each case
> describing what the component should do depending on a specific
> situation (or mode) the component is in.
>
> This talk introduces CoCoSpec, a mode-aware assume-guarantee-based
> contract language for embedded systems. CoCoSpec is built as an
> extension of the Lustre language and lets users specify mode behavior
> directly, instead of encoding it as conditional guarantees, thus
> preventing a loss of mode-specific information. Mode-aware model
> checkers supporting CoCoSpec can increase the effectiveness of the
> compositional analysis techniques found in assume-guarantee frameworks
> and improve scalability. Such tools can also produce much better
> feedback during the verification process, as well as valuable
> qualitative information on the contract itself. I will presents the
> CoCoSpec language and illustrate the benefits of mode-aware
> model-checking on a case study involving a flight-critical avionics
> system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based
> model checker developed at the University of Iowa that provides full
> support for CoCoSpec.
>
> Bio:
>
> Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in
> 1999 and is currently a professor in Computer Science at the University
> of Iowa. His research interests include automated reasoning and formal
> methods. He has done seminal work in automated reasoning, in particular
> in Satisfiability Modulo Theories (SMT), a field he helped establish
> through his research and service activities. His work has been funded
> both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and
> corporations (Intel, General Electric, Rockwell Collins, and United
> Technologies) and has appeared in more than 70 refereed publications. He
> is a founder and coordinator of the SMT-LIB initiative, an international
> effort aimed at standardizing benchmarks and I/O formats for SMT
> solvers. He has led the development of the award winning Darwin theorem
> prover and the Kind model checker. He co-leads the development of CVC4,a
> widely used and award winning SMT solver, and StarExec, a cross
> community web-based service for the comparative evaluation of logic
> solvers.