Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Speakers and Abstracts

Verified Software Workshop and Summer School 2012

Nikolaj BjornerNikolaj Bjorner
Senior Researcher
Microsoft Research Redmond

Bio: Nikolaj Bjorner is a senior researcher in the Research in Software Engineering group at Microsoft Research, Redmond. His main line of work focuses on the state-of-the-art SMT constraint solver Z3 with Leonardo de Moura. Z3 is used for program verification and test-case generation. Previously, he wrote STeP, the Stanford Temporal Prover, and was in the Core File Systems group where he designed and implemented the core of the distributed file replication system, DFS-R, and the content dependent chunking algorithms in the remote differential compression protocol RDC.

Presentation Title: Modern Satisfiability Modulo Theories Solvers in Program Analysis

Abstract: Satisfiability Modulo Theories (SMT) solvers have advanced rapidly over the last decade and are able to deal with problems from large-scale applications. A significant application domain for SMT solvers is in the analysis, verification, testing, and construction of programs. This course will give an introduction to SMT solving and hands-on experience with the state-of-the art Z3 SMT solver from Microsoft Research. We also connect the capabilities of SMT solvers with several applications from program analysis.

Jin-Song DongJin-Song Dong
Associate Professor
National University of Singapore

Bio: Jin-Song Dong received Bachelor (first-class hon) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995 to1998, he was research scientist at CSIRO in Australia. Since 1998 he has been in the School of Computing at the National University of Singapore (NUS) where he is currently associate professor and a member of PhD supervisors at NUS Graduate School. He is the deputy director of Singapore-French joint Research lab IPAL. Jin Song is on the editorial board of Formal Aspects of Computing Journal and Innovations in Systems and Software Engineering, A NASA Journal. He has been steering committee member and general/program chair for a number of international conferences. Jin Song has been a visiting fellow (2006) at Oxford University, UK, and a visiting professor (since 2009) at National Institute of Informatics, Japan. His research interests include formal methods, software engineering, pervasive computing, and semantic technologies.

Presentation Title: Pervasive Model Checking

Abstract: Popular model checkers like SPIN, SMV, and FDR are designed for specialized domains and are based on restrictive modeling languages. In this talk, we introduce our latest work on combining the expressiveness of state, event, real-time, and probability-based languages with the power of model checking. We present the process analysis toolkit (PAT), which is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 15 different modeling formalism/languages, including CSP# (short for “communicating sequential programs,” which is based on Hoare’s CSP). The idea is to treat sequential terminating programs—which may indeed be C# programs—as internal events. The result is a highly expressive modeling language which covers many application domains. PAT’s pervasive model checking vision also includes applying model checking as planning, scheduling and problem solving services. Since PAT was released four years ago, it has attracted more than 1,700 registered users from more than 350 organizations in more than 40 countries.

Masahiro Fujita
Professor
University of Tokyo

Bio: Prof. Masahiro Fujita received his Ph.D. in Information Engineering from the University of Tokyo in 1985 on his work on model checking of hardware designs by using logic programming languages. In 1985, he joined Fujitsu as a researcher and started to work on hardware automatic synthesis as well as formal verification methods and tools, including enhancements of BDD/SAT-based techniques. From 1993 to 2000, he was director at Fujitsu Laboratories of America and headed a hardware formal verification group developing a formal verifier for real-life designs having more than several million gates. The developed tool has been used in production internally at Fujitsu and externally as well. Since March 2000, he has been a professor at VLSI Design and Education Center of the University of Tokyo. He has done innovative work in the areas of hardware verification, synthesis, testing, and software verification—mostly targeting embedded software and web-based programs. He has been involved in a Japanese governmental research project for dependable system designs and has developed a formal verifier for C programs that could be used for both hardware and embedded software designs. The tool is now under evaluation jointly with industry under governmental support. He has authored and co-authored 10 books, and has more than 200 publications. He has been involved as program and steering committee member in many prestigious conferences on CAD, VLSI designs, software engineering, and more. His current research interests include synthesis and verification in SoC (System on Chip), hardware/software co-designs targeting embedded systems, digital/analog co-designs, and formal analysis, verification, and synthesis of web-based programs and embedded programs.

Presentation Title: Formal Analysis and Verification of Multiple Programs Based on Difference Identification

Abstract: There have been many research efforts in software formal analysis and verification. Although software normally has multiple versions, most of the techniques for software analysis and verification developed so far deal with each version individually. From a practical viewpoint, however, people like to understand what parts are the same or functionally equivalent and what parts are different in those various versions of the programs. With a good understanding of those issues, programs can be correctly used and adequately maintained and enhanced. In this talk, we show a method by which functional equivalence and different portions of the multiple programs can be identified. The proposed method first translates given programs into virtual assemblies and then analyzes them with varieties of textual and graph-based techniques for identification of difference, symbolic simulation-based identification of equivalence/non-equivalence, and dependence graph-based formal analysis. With the proposed method, formal equivalence verification among subsets of multiple programs can be performed very quickly, and regression tests can be much more efficient. Also, program reuse could be much more error free and quickly applied under various conditions.

Patrice GodefroidPatrice Godefroid
Principal Researcher
Microsoft Research Redmond

Bio: Patrice Godefroid is a principal researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at Bell Laboratories (part of Lucent Technologies), where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program (mostly software) specification, analysis, testing and verification.

Dr. Godefroid is probably best known for his pioneering work on partial-order reduction for model checking concurrent systems (his PhD thesis is published as LNCS volume 1032 by Springer), for his work on VeriSoft, the first software model checker for mainstream programming languages such as C and C++, for his work on 3-valued model checking with may/must abstractions for sound program verification and falsification, and for his work on automatic test generation with DART. More recently, he co-developed SAGE, the first white box fuzzer for security testing, which was credited to have found roughly one third of all the security vulnerabilities discovered by file fuzzing during the development of Microsoft's Windows 7.

Presentation Title: Software Model Checking

Abstract: Over the last two decades, significant progress has been made on how to broaden the scope of model checking from finite-state abstractions to actual software implementations. The aim of these lectures is to present a partial yet comprehensive overview of software model checking, by describing the main ideas, techniques and results obtained in this area, including connections to static program analysis and testing.

Aarti Gupta Aarti Gupta
Department Head, Systems Analysis and Verification
NEC Labs America

Bio: Aarti Gupta received a B. Tech. in Electrical Engineering from IIT Delhi (India), and a Ph.D. in Computer Science from Carnegie Mellon University. Her research interests are broadly in the areas of formal verification, automatic decision procedures, and program analysis.

Aarti currently leads the Systems Analysis and Verification Group at NEC Laboratories America (Princeton, United States). The group engages in foundational as well as applied research in analysis of systems, bringing together the domains of system modeling, automatic verification, program analysis, and software testing. These research efforts have been incorporated in internal products within NEC that have been deployed for static verification of software programs.

Aarti has published at leading international conferences and journals. She has served on the technical program committees of many conferences, including serving as co-chair (IEEE/ACM Conference on Formal Methods in Computed Aided Design 2006, International Conference on Computer Aided Verification 2008). She is currently serving as an associate editor for Formal Methods in System Design, and ACM Transactions on Design Automation of Electronic Systems.

Presentation Title: Detecting Concurrency Bugs using Static and Dynamic Program Analyses

Abstract: The proliferation of multi-core hardware has led to widespread use of concurrent programs. However, these programs are difficult to develop and debug, requiring reasoning about subtle synchronizations and interleavings between threads/processes. In this talk, I will describe three main approaches we have used to find concurrency bugs, spanning a range of static and dynamic program analyses.

  • The first is a layered program decomposition framework for scalable static data race detection. Here we address the goals of precision (by using flow and context-sensitive points-to analysis) and scalability (by decomposing the program control flow graph into layers of bounded call-depth). This framework has been successfully applied on large industry projects to find data races.
  • The second approach uses predictive analysis, where a predictive model is derived from a test execution to capture alternate interleavings of the same events. We use symbolic prediction, based on Satisfiability Modulo Theories (SMT) solvers, to find data races and atomicity violations.
  • The third approach is based on systematic testing, where we use a coverage-based metric to guide the selection of interleavings to explore. Although unsound, the metric works well to catch many bugs in practice, while significantly improving performance in comparison to exhaustive state-space exploration.

Shi HanShi Han
Associate Researcher
Microsoft Research Asia

Bio: Shi Han is an associate researcher at the Software Analytics group of Microsoft Research Asia. His research interests include data-driven software analysis, machine learning, and large-scale computing platform. Incorporating expertise from these domains, he has been pursuing research on performance analysis for large-scale system software. Since 2009, he has been the key contributor to StackMine—a scalable stack trace mining platform for Windows performance debugging in the large. Before 2009, he was a key contributor to the algorithm design and implementation of the HMM-based East Asian character handwriting recognition engine in Windows 7.

Presentation Title: Software Analytics and Its Application in Software Development Practice

Abstract: A huge wealth of various data exists in the software lifecycle, including source code, feature specifications, bug reports, test cases, execution traces/logs, and real-world user feedback. Data plays an essential role in modern software development, because hidden in the data is information about the quality of software and services as well as the dynamics of software development. With various analytical and computing technologies, software analytics enable software practitioners to perform effective and efficient data exploration and analysis in order to obtain insightful and actionable information for data-driven tasks in engineering software and services. In this talk, I will introduce the software analytics research in Microsoft Research Asia and I will also share our experiences on how we utilize our research results to help solve some real problems in software development at Microsoft.

Jifeng He
Professor, Software Engineering Institute, East China Normal University
Member of Chinese Academy of Sciences

Bio: Jifeng He graduated in 1965 from Fudan University majoring in mathematics. He is currently the dean of the Institute of Software of East China Normal University. Prof. He's research interests include credible and information security theory, formal method, concurrent programming, theory, embedded system design methods and tools, hybrid system hardware, and software co-design computer software and theory. He was elected a member of Chinese Academy of Sciences in 2005.

Presentation Title: Linking the Discrete World with Continuous World

Tony HoareTony Hoare
1980 Turing Award Winner
Principal Researcher, Microsoft Research Cambridge

Bio: Tony Hoare and his family first visited China in 1983, with Cliff Jones and family. They both gave lectures at the Graduate School of the Chinese Academy of Sciences. He has visited China three more times since 2000. He was a keynote lecturer at IFIP 2000, and an Einstein Professor of the Chinese Academy in 2006.

Tony Hoare's interest in computing was awakened in the early 1950s, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth. During his National Service (1956–1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally, a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.

On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of chief engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as chief scientist to the computing research division, where he worked on the hardware and software architecture for future machines. These machines were cancelled when the company merged with its rivals, and in 1968 Tony took a chance to apply for the professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.

In 1977, he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in computer science, including an external master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.

Throughout more than 30 years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.

Presentation Title: Theory for Verified Software

Abstract: Tony Hoare will present his current approach to Unifying Theories of Programming. It unifies sequential and concurrent programming, using ideas from separation logic. Every tool that is used for software verification must be based on a theory of programming (sometimes called semantics). The use of tools in combination requires the definition of an interface, based on a theory that unifies the theories on which the separate tools are based. As in other branches of science, he hopes that this unifying theory can be simpler than the theories which it unifies. His new approach uses pictorial representations from labeled graph theory, in place of the relational calculus used in the book by Hoare and He. It should therefore be suitable for non-theorists

Evening Seminar: Night of Theory for Verified Software

Abstract: In this special evening seminar, chaired by Tony Hoare, all theory track speakers will be invited to give a survey of historic and recent research in their fields of expertise, and to describe research problems. The seminar is specifically designed for faculty and senior graduate students who specialize in verified software theory.

Sun JunSun Jun
Assistant Professor
Singapore University of Technology and Design

Bio: Sun Jun is interested in developing systematic tools, theories, and methodologies for software/system correctness, reliability, and efficiency. He currently focuses on automated system verification techniques, in particular, model checking and has developed a model-checking framework called PAT. He earned his PhD from the School of Computing at the National University of Singapore. Learn more.

Presentation Title: Case Studies Using PAT

Abstract: This talk will briefly introduce the PAT model checking framework and then focus on two real-world case studies. The first case study applies PAT to a pervasive computing system, in particular, a smart nursing home for elderly or mild dementia patients. Through manual modeling, PAT is used to capture behaviors of sensors, patients as well as the reasoning engine which generates high-level context information from low-level sensory inputs. The second case study applies model checking to a number of widely used security protocols. Models are generated through reserve-engineering of implementations as well as general domain knowledge. In both cases, a number of bugs have been identified and later fixed.

Daniel Kroening Daniel Kroening
Professor of Computer Science
University of Oxford

Bio: Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbruecken, Germany, in 1999 and 2001, respectively. He joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA, United States, in 2001 as a post-doc. He was an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, from 2004 to 2007. He is now professor at the Computer Science at Oxford University. His research interests include automated formal verification of hardware and software systems, decision procedures, embedded systems, and hardware/software co-design.

Presentation Title: Verifying Concurrent Software

Abstract: We discuss how to apply predicate abstraction to programs that feature shared-variable concurrency. We begin by demonstrating how to exploit symmetry in the abstract model to improve the scalability of the analysis. Finally, we show how to reason about programs in which the number of threads has no a-priori bound.

Akash LalAkash Lal
Researcher
Microsoft Research India

Bio: Akash Lal is a researcher at Microsoft Research, Bangalore. His interests are in the area of programming languages and program analysis. He joined Microsoft in 2009 and devotes most of his time towards building automated bug-finding tools for concurrent systems. He completed his PhD at the University of Wisconsin-Madison under the supervision of Prof. Thomas Reps. For his thesis, he received the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He completed his bachelor's degree at IIT-Delhi in 2003.

Presentation Title: Bounding and Sequentializing Concurrent Programs

Abstract: Software defects that are the result of concurrency and asynchrony are difficult to find, reproduce, and fix. In fact, the non-local control flow that concurrency or asynchrony induce fundamentally raises the complexity of analyzing such programs. Consequently, while many automated tools for sequential programs exist, there are relatively few for concurrent programs.

In this talk, I will present a recent trend towards bridging this gap by using sequential tools to analyze concurrent programs. This is based upon two key concepts. First is the observation that many concurrency-related bugs are exposed in very simple scenarios, for example, those with a low number of context switches. Thus, a bounded exploration can reveal many bugs. Second, all concurrent behaviors under a fixed bound can be succinctly captured by using a sequential program—a technique that is now commonly known as sequentialization. This allows one to directly apply sequential program-analysis tools to conduct bounded exploration of concurrent programs.

My talk will also cover several different notions of bounding (for capturing common bugs) and their corresponding sequentialization (for efficient analysis) for different kinds of concurrency paradigms (like multi-threading, asynchrony or event-driven programs, and distributed systems).

Jing LiuJing Liu
Professor
East China Normal University

Presentation Title: Spatio-Temporal UML Profile for Cyber-Physical Systems

Abstract: Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Therefore, both time and space information are required in the design and modeling of CPS systems. CPS also requires demanding real-time property. However, unified modeling of continuous and discrete variables is still an unsolved problem in the CPS development. Spatio-Temporal UML statechart is an extended UML statechart, developed for Cyber-Physical Systems (STUML Statechart). This statechart is based on the UML Profile for Modeling and Analysis of Real-time and Embedded (MARTE) systems. In STUML Statecharts, we unify the logical time and the chronometric time variables, and extend the traditional events to CPS events. Based on MARTE and hybrid automata, we improve the STUML statechart, and based on Labeled Transition Systems, we define formal syntax and semantics of STUML statecharts. An Intelligent Transportation System is modeling based on STUML and shows how to model the system behavior with STUML statecharts.

Matthew ParkinsonMatthew Parkinson
Researcher
Microsoft Research Cambridge

Bio: Matthew Parkinson is a researcher at Microsoft Research Cambridge. He is working on software verification for concurrent programs. Prior to joining Microsoft, he spent four years in the Cambridge Computer Lab on an RAEng/EPSRC research fellowship investigating how to verify that object-oriented and concurrent programs meet their specifications. Before the research fellowship, he did a post-doc with Richard Bornat verifying crazy concurrent programs running on exotic hardware. Prior to that, he was a Ph.D. student in the Computer Lab at the University of Cambridge working with Gavin Bierman on extending separation logic to reason about Java programs.

Presentation Title: Separation Logic

Rasmus Lerchedahl PetersenRasmus Lerchedahl Petersen
Research Developer
Queen Mary University of London

Bio: Rasmus Lerchedahl Petersen received his Ph.D. from the IT University of Copenhagen in 2007 where he studied the semantics of programming languages. He then went on to work on automated verification of programs via static analysis and reasoning principles for concurrency at Queen Mary University in London. He is now part of the Biological Computation group at Microsoft Research, Cambridge.

André PlatzerAndré Platzer
Assistant Professor
Carnegie Mellon University

Bio: André Platzer is an assistant professor in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA. Prof. Platzer's interests include logical foundations of cyber-physical systems, hybrid systems, distributed hybrid systems, stochastic hybrid systems, logic in computer science, automated theorem proving, model checking, and symbolic and numerical computation. Dr. Platzer developed the theory, practice, and applications of logic-based verification of hybrid systems, and he proved the first completeness theorem for hybrid systems. He introduced compositional verification techniques and the technique of differential invariant that can verify hybrid systems without solving their differential equations. In addition, he led the development of the first theorem prover for hybrid systems (KeYmaera) and he has verified aircraft, train control, and car control systems.

André Platzer obtained a master's degree in computer science from the University of Karlsruhe (TH), Germany, in 2004, and a Ph.D. in computer science from the University of Oldenburg, Germany, in 2008.

Among other awards, Dr. Platzer received an ACM Doctoral Dissertation Honorable Mention Award 2009, an NSF CAREER Award 2011, the Best Paper Awards at TABLEAUX'07 and at FM'09. André Platzer was also named one of the Brilliant 10 Young Scientists by Popular Science magazine (2009) and was named one of the AI's 10 to Watch 2010 by IEEE Intelligent Systems Magazine.

Presentation Title: Logical Analysis of Hybrid Systems: The KeYmaera Approach

Abstract: Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. Because these systems operate in the physical world, stringent safety requirements are usually imposed on cyber-physical system designs. There is a well-understood theory for guaranteeing correct functioning of computer programs using logic and formal verification techniques. But what about cyber-physical systems? How can we ensure that cyber-physical systems are guaranteed to meet their design goals, for example, that an aircraft cannot crash into another one?

This talk describes how logic and formal verification can be lifted to hybrid systems. It presents the theoretical and practical foundations of logical analysis of hybrid systems. The talk describes a logic for hybrid systems called differential dynamic logic and gives a perfectly compositional proof technique, including differential invariants, an induction technique for differential equations. This logical approach is implemented in the verification tool KeYmaera and has been used successfully for verifying nontrivial properties of aircraft, railway, and car control applications. The logical approach is also interesting from a theoretical perspective, because it shows how verification techniques for continuous dynamics can be lifted to hybrid systems by a complete axiomatization.

Shaz Qadeer
Senior Researcher, Research in Software Engineering
Microsoft Research Redmond

Bio: Shaz Qadeer is a senior researcher in Microsoft Research. He received his Ph.D. from the University of California at Berkeley. He has worked at Microsoft Research for most of his professional life, except for a short period at Compaq Systems Research Center and an even shorter period at HP Labs. Shaz develops tools and techniques for making programming better and easier; in particular, he is trying to simplify the construction of concurrent and parallel programs.

Presentation Title: Safe Programming of Asynchronous Interaction: Can We Do It for Real?

Abstract: USB is the most successful peripheral interface in the history of personal computing with billions of existing devices and billions more being sold every year. Windows 8 will ship with a brand new driver stack for USB devices. The design of this software stack was powered by an unprecedented use, early in the development cycle, of a programming methodology based on formal modeling and verification of asynchronously-interacting state machines. This work had significant impact, yet it suffers from limitations whose primary manifestation is a high barrier-to-entry for new programmers. To address these limitations, we are developing a new system for developing programs composed of interacting state machines. The new programming environment provides easy specification and visualization of state machines, comprehensive verification early in the design process, and efficient code generation. The verification capabilities of our system rest on two foundations—fast checking of syntactic properties via static analysis and potentially expensive checking of semantic properties via state exploration. If time permits, I will present a demonstration of the new programming environment.

Jan-David Quesel Jan-David Quesel
Research Assistant
University of Oldenburg, Germany

Bio: Jan-David Quesel is a research assistant at the University of Oldenburg, Germany. In his diploma thesis (MSc), he developed, under supervision of André Platzer, KeYmaera, a theorem prover for hybrid systems based on the proof calculus for differential dynamic logic. Since June 2007, he is working for his PhD, under supervision of Ernst-Ruediger Olderog, on the topic of hybrid system similarity. His research interests range from the verification of hybrid and timed systems, semantics of those, and logics to theorem proving and model-checking. Recently, he expanded his field of research towards hybrid game theory.

Jianqi Shi
East China Normal University

Presentation Title: ORIENTAIS: a Formal Verified OSEK/VDX Real-Time Operating System

Abstract: In this section, we report on the formal, machine-verified operating system: ORIENTAIS. ORIENTAIS is an OSEK/VDX standard based real-time operating system for automotive applications. About 8,000 lines of C and 60 lines of assembler are comprised in the ORIENTAIS. The operating system is of vital importance to embedded systems, especially for some time-sensitive and accurate controlling applications just like automotive applications. We prove that the implementation of ORIENTAIS application programming interfaces strictly follow the OSEK/VDX specification that we formalized from natural language expressed OSEK/VDX specification. The specification verification is based on binary code. Meanwhile, to guarantee the safety of memory access and bounded response time with interrupt program involved, binary code level verification is developed based on xBIL which is a binary intermediate language we proposed. We introduce a series of techniques and approaches for verifying the ORIENTAIS. Our approach is an efficient work for the verification of ORIENTAIS, with whose help several bugs are detected. Now, ORIENTAIS has been certificated by the OSEK certification group and installed on more than 1.38 million cars in China. In the presentation, the process of the operating system verification will be introduced and approaches in each verification phase will be demonstrated.

Georg Struth
Reader
University of Sheffield

Bio: Georg Struth is a reader in computer science at the University of Sheffield, UK. He studied physics and philosophy at the Universities of Mainz and Heidelberg and received a PhD in Computer Science from Saarland University/Max Planck Institute for Computer Science in 1999. He joined the University of Sheffield in 2005.

Georg Struth is best known for his work on algebraic methods in computer science, including Kleene algebras and modal algebras, but his research interests also include automated and interactive theorem proving, software verification, and, more recently, concurrency theory.

Presentation Title: Algebra for Concurrency

Abstract: Building on Tony Hoare's first lecture, this talk starts by developing a simple semigroup-based approach to concurrency, in which the main emphasis is on the interaction between sequential and concurrent composition. Models of interleaving and true concurrency, including a new partial trace model, serve as a motivation. The algebra is then enriched by operations for nondeterministic choice, iteration, and residuation; notions of Hoare triple and partial correctness are defined. It supports a particularly simple derivation of a basic Hoare logic for modular reasoning about concurrent programs, which is inspired by concurrent separation logic. Kleene algebras are now widely perceived as foundational models and tools for reasoning about sequential programs. The algebras outlined in this lecture are intended to yield similar models and tools in the realm of concurrency.

Zheng Wang
East China Normal University

Presentation Title: SPARDL: a Modeling Framework for Periodic Control System

Abstract: Periodic control systems used in safety-critical embedded domains, such as spacecraft, avionics and automotive control are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such systems may also involve intensive computing in their modes. Despite the fact that such control systems are widely used in the above-mentioned safety-critical embedded domains, there is lack of domain-specific formal modeling languages for such systems in the relevant industry.

To address this problem, we propose a formal visual modeling framework called SPARDL as a concise and precise way to specify and analyze such systems. To capture the temporal properties of periodic control systems, we provide, along with the modeling notation, a property specification language based on interval temporal logic. Some static analysis techniques such as type checking, dataflow analysis are applied on the formal models. The statistical model checking technique can then be used to verify the SPARDL models against desired properties.

Chaochen ZhouChaochen Zhou
Professor, Institute of Software, Chinese Academy of Sciences
Member of Chinese Academy of Sciences

Bio: Chaochen Zhou graduated from the Department of Mathematics and Mechanics, Peking University, in 1958, and received his postgraduate degree from the Institute of Computing Technology, Chinese Academy of Sciences, in 1967. He has been a research professor of Institute of Software since 1986. He was elected as a member of Chinese Academy of Sciences in 1993, and a member of the Third World Academy of Sciences in 2000. His research interests include distributed and real-tim computing systems.

Presentation Title: Modeling and Verification of Hybrid Systems

Abstract: A hybrid system is a mixture of discrete actions and continuous evolutions. The lecture introduces and explains a modeling language for hybrid systems: Hybrid CSP. Hybrid CSP includes assignments, synchronous communications over channels, differential equations over time and interruptions caused by boundary, time-out, and communication. It also includes sequential as well as parallel operators. In order to verify real-time properties of hybrid systems—i.e. processes of Hybrid CSP—we establish a calculus based on Hoare Logic and Duration Calculus. The calculus is called Hybrid Hoare Logic, which uses differential invariants to interpret differential equations. An algorithm for discovering polynomial differential invariants is also presented in the lecture.

Dates
  • Workshop: August 23–24, 2012
  • Summer School: August 27–31, 2012
Venue

East China Normal University
Shanghai, China

Related Links