HILT 2013             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Conference at a Glance

Final Program

Sunday, November 10
Morning Tutorials (9:00am - 12:30pm)
SA1 Object-Oriented Programming in Ada 2012, Part 1
Ed Colbert (Absolute Software)
SA2 Proving Safety of Parallel / Multi-Threaded Programs
Tucker Taft (AdaCore)
Afternoon Tutorials (2:00 - 5:30pm)
SP1 Object-Oriented Programming in Ada 2012, Part 2
Ed Colbert (Absolute Software)
SP2 Engineering Domain-Specific Languages with FORMULA 2.0
Ethan K. Jackson (Microsoft Research)

Monday, November 11
Morning Tutorials (9:00am - 12:30pm)
MA1 Satisfiability Modulo Theories for High Integrity Development
Nikolaj Bjorner (Microsoft Research)
MA2 Practical Specification and Verification with CodeContracts
Francesco Logozzo (Microsoft Research)
Afternoon Tutorials (2:00 - 5:30pm)
MP1 Bounded Model Checking for High-Integrity Software
Sagar Chaki (Carnegie Mellon University Software Engineering Institute)
MP2 Service-Oriented Architecture (SOA) Concepts and Implementations
Ricky E. Sward (The MITRE Corporation)
Jeff Boleng (Carnegie Mellon University Software Engineering Institute)
Evening Activities (7:00pm - 10:00pm)
7:00 - 10:00pm SIGAda Extended Executive Committee (EEC) Meeting
(Open to all)

Tuesday, November 12
TECHNICAL PROGRAM - Technology for Program Verification
9:00 - 10:30am

Greetings from SIGAda and Conference Officers

Keynote Address:

Model Checking and the Curse of Dimensionality
Edmund M. Clarke
(CMU BioSketch; Wikipedia BioSketch)
(Carnegie Mellon University
2007 ACM Turing Award)

10:30 - 11:00am Morning Break - Exhibits Open
11:00am - 12:30pm
Session: Underlying Formal Verification Technologies

Panel: Underlying Formal Verification Technologies

Moderator: Tucker Taft (AdaCore)

Coq-based Proofs — Prof. Robby (Kansas State University)
SMT Solvers — Nikolaj Bjorner (Microsoft Research)
Technology for Inferring Contracts from Code — Francesco Logozzo (Microsoft Research)
Bounded Model Checking — Sagar Chaki (Carnegie Mellon University Software Engineering Institute)

AdaCore Sponsor Presentation
Albert Lee (AdaCore)

12:30 - 2:00pm Mid-day Break and Exhibits
2:00 - 3:30pm
Session: Formal Verification Toolsets

SAW: The Software Analysis Workbench
Joe Hendrix (Galois)

Optimising Verification Effort with SPARK 2014
Andrew Hawthorn (ALTRAN)

Towards the Formalization of SPARK 2014 Semantics with Explicit Run-time Checks Using Coq
Zhi Zhang (Kansas State University)

3:30 - 4:00pm Afternoon Break & Exhibits
4:00 - 5:30pm
Session: High-Integrity Parallel Programming

Panel: Safe, Efficient Parallel Programming

Moderator: Clyde Roby (Institute for Defense Analyses)

Real-Time Programming on Accelerator Many-Core Processors — Stephen Michell (Maurya Software)
Bring Safe, Dynamic Parallel Programming to the SPARK Verifiable Subset of Ada — Tucker Taft (AdaCore)

Verocel Sponsor Presentation
George Romanski (Verocel)

5:30 - 6:30pm Break
6:30 - 10:00pm

Evening Social Event
Pittsburgh Athletic Association

Wednesday, November 13
TECHNICAL PROGRAM - Model-Based Engineering and Verification
9:00 - 10:30am


SIGAda Awards
Ricky E. Sward

Overall Introduction to Model-Based Engineering and Verification Day
Julien Delange (Carnegie Mellon University Software Engineering Institute (SEI))

Invited Address

Up and Out: Scaling Formal Analysis Using Model-Based Development and Architecture Modeling
Michael Whalen (University of Minnesota)

10:30 - 11:00am Morning Break and Exhibits
11:00am - 12:30pm
Session: Model-Based Integration and Code Generation

An Approach to Integration of Complex Systems: The SAVI Virtual Integration Process (industrial presentation)
David Redman (Aerospace Vehicle Systems Institute)

Reddo - A Model Driven Engineering Toolset for Embedded Software Development (industrial presentation)
Steven Doran (Northrop Grumman Corporation)

Ellidiss Sponsor Presentation
Tony Elliston (Ellidiss (TNI Europe))

12:30 - 2:00pm Mid-day Break and Exhibits
(Exhibits close at 2:00pm)
2:00 - 3:30pm

Keynote Address:

Building Confidence in System Behavior
John Goodenough
(CMU/SEI BioSketch)
(Carnegie Mellon University Software Engineering Institute)

3:30 - 4:00pm Afternoon Break
4:00 - 5:30pm
Session: Architecture-Level Design Languages and Compositional Verification

Compositional Verification of a Medical Device System
Sanjai Rayadurgam (University of Minnesota)

Illustrating the AADL Error Modeling Annex (v.2) Using a Simple Safety-Critical Medical Device
Brian Larson (Kansas State University)

Microsoft Research Sponsor Presentation
Ethan K. Jackson (Microsoft Research)

5:30 - 7:00pm Dinner Break
7:00 - 10:00pm
Session: Birds-of-a-Feather (BoF) and Workshops

Birds of a Feather: GNAT Users
Albert Lee (AdaCore)

Thursday, November 14
TECHNICAL PROGRAM - Applying Formal Methods to the Real World
9:00 - 10:30am


Best Paper and Student Paper Awards
Tucker Taft

Keynote Address:

Formal Methods: An Industrial Perspective
Jeannette Wing
(Microsoft Research BioSketch; Wikipedia BioSketch)
(Microsoft Research)

10:30 - 11:00am Morning Break
11:00am - 12:00pm
Session: Approaches to Software Safety and Security

Panel: Approaches to Software Safety and Security

Moderator: Alok Srivastava (TASC Inc.)

Secure Coding — Robert Seacord (SEI/CERT)
Use of Domain-Specific Languages — Ethan K. Jackson (Microsoft Research)
Integrating technologies for verification — Joe Hendrix (Galois)
Using contract-based programming tools — Francesco Logozzo (Microsoft Research)
Automatic versus Interactive Program Verification — Suad Alagic (University of Southern Maine)

12:00 - 12:30pm

Ada-Europe 2014 Conference Announcement
Dirk Craeynest

SIGAda 2014 Conference Announcement
Tucker Taft

12:30pm Closing Comments & Conference Adjournment

Created on 29 May 2014;  website comments and corrections to ClydeRoby at ACM.Org