Program
All talks will be in ERF 1043. The tentative MVD'13 schedule can be found here. Please check the schedule regularly as it is subject to change.
Raymond Richard's talk titled "Rockwell Collins and Formal Methods" can be found here.
Invited Speakers
Key Note Speaker: Tom Ball
Time and Location: 9:15 AM, 9/20/2013 in ERF 1043
Title: Advances in Automated Theorem Proving and Applications
Abstract: In the last decade, advances in satisfiability-modulo-theories (SMT) solvers have powered a new generation of software tools for verification and testing. These tools transform various program analysis problems into the problem of satisfiability of formulas in propositional or first-order logic, where they are discharged by SMT solvers, such as Z3 from Microsoft Research (MSR). In this talk, I’ll review advances from MSR that expand the scope of SMT solvers on several fronts. These advances are due to Nikolaj Bjorner, Leonardo de Moura, Ken McMillan, and Margus Veanes at MSR, and their colleagues and interns.
Bio: Thomas Ball (Tom) is a Principal Researcher and Research Manager at Microsoft Research. Tom graduated with a B.A. in Computer Science from Cornell University in 1987 and a M.S. and Ph.D. from the University of Wisconsin-Madison in 1993. From 1993-1999, he was a member of the technical staff at Bell Laboratories, where he made contributions in program visualization and profiling. In 1999, Tom moved to Microsoft Research, where he started the SLAM software model checking project with Sriram Rajamani, which led to the creation of the Static Driver Verifier (SDV) tool for finding defects in device driver code. Tom and Sriram received the 2011 CAV Award "for their contributions to software model checking, specifically the development of the SLAM/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs." Tom is a 2011 ACM Fellow for "contributions to software analysis and defect detection". Since becoming a manager at Microsoft, he has nurtured research areas such as automated theorem proving, program testing/verification, and empirical software engineering. Tom performed this summer in the Seattle Opera chorus in Wagner’s Ring cycle. He is a member of the ACM and the American Guild of Musical Artists.
A copy of Dr. Ball's talk can be found here.
Invited Speaker: Robert V. Binder
Time and Location: 9:00 AM, 9/21/2013 in ERF 1043
Title: Hunting the Dragon-King: Multi-Dimensional Testing
Abstract: This talk presents multi-dimensional testing, a model-based strategy to produce test suites that interleave non-trivial variation in system usage and load. Compared with equivalent but separate usage and load test suites, this achieves testing that is highly realistic and more likely to reveal catastrophic failure modes. A project in which this approach was evolved and used is described. An innovative model of system failure, the “dragon king” provides a useful model of failure modes in large reactive systems, providing insight into recent high profile failures of complex distributed systems. I argue that multi-dimensional testing is necessary to reveal dragon-kings.
Bio:Robert V. Binder is a serial entrepreneur, high assurance thought-leader, and system architect.
As President of System Verification Associates, he has provided assurance solutions for clients facing existential regulatory challenges. He is internationally recognized as the author of the definitive Testing Object-Oriented Systems: Models, Patterns, and Tools and two other books. He is a member of the Editorial Board of the Journal of Software Testing, Verification, and Review.
He is currently co-director of the UIC Internet Assurance Lab and co-chair of X9 D14 working group developing a management standard for automated trading systems.
Binder received the MS in Electrical Engineering and Computer Science from the University of Illinois at Chicago and the BA and MBA from the University of Chicago. He is an IEEE Senior Member and holds the CSDP.
A copy of Robert Binder's talks can be found here.