HILT 2012 Final Program

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Conference at a Glance

Final Program

Sunday, December 2
TUTORIAL PROGRAM
Full-Day Tutorials (9:00am - 5:30pm)
SF1	Design of multitask software: The entity-life modeling approach Bo I. Sandén (Colorado Technical University)
Morning Tutorials (9:00am - 12:30pm)
SA1	Leading-edge Ada Verification Technologies: Highly automated Ada contract checking using Bakar Kiasan Jason Belt (Kansas State University) Patrice Chalin (Kansas State University) John Hatcliff (Kansas State University) Dr. Robby (Kansas State University)
SA2	Ada 2012 Contracts and Aspects Ed Colbert (Absolute Software)
Afternoon Tutorials (2:00 - 5:30pm)
SP1	Leading-Edge Ada Verification Technologies: Combining Testing and Verification with GNATTest and GNATProve — the Hi-Lite Project Johannes Kanig (AdaCore)
SP2	Object-Oriented Programming with Ada 2005 and 2012 Ed Colbert (Absolute Software)

Monday, December 3
TUTORIAL PROGRAM
Full-Day Tutorials (9:00am - 5:30pm)
MF1	Safety of Embedded Software Nancy Leveson (Massachusetts Institute of Technology) Cody Fleming (Massachusetts Institute of Technology) John Thomas (Massachusetts Institute of Technology)
Morning Tutorials (9:00am - 12:30pm)
MA1	Developing Verified Programs with Dafny K. Rustan M. Leino (Microsoft Research)
MA2	Service-Oriented Architecture (SOA) Concepts and Implementations Ricky E. Sward (The MITRE Corporation) Jeff Boleng (Software Engineering Institute)
Afternoon Tutorials (2:00 - 5:30pm)
MP1	Multicore Programming using Divide-and-Conquer and Work Stealing Tucker Taft (AdaCore)
MP2	Understanding Dynamic Memory Management in Safety Critical Java Kelvin Nilsen (Atego, Inc.)
Evening Activities (7:00pm - 10:00pm)
7:00 - 10:00pm	SIGAda Extended Executive Committee (EEC) Meeting (Open to all)

Tuesday, December 4
TECHNICAL PROGRAM - Analyzing and Proving Programs
9:00 - 10:30am	Greetings from SIGAda and Conference Officers Keynote Address: Programming the Turing Machine (Abstract) Barbara Liskov (Massachusetts Institute of Technology Department of Electrical Engineering and Computer Science)
10:30 - 11:00am	Morning Break - Exhibits Open
11:00am - 12:30pm	Session: Program Verification at Compile-Time Program Proving using Intermediate Verification Languages (IVLs) like Boogie and Why3 K. Rustan M. Leino (Microsoft Research) Hi-Lite: The Convergence of Compiler Technology and Program Verification Claire Dross (AdaCore), Johannes Kanig (AdaCore), and* Edmond Schonberg (AdaCore)* Microsoft Research Sponsor Presentation
12:30 - 2:00pm	Mid-day Break and Exhibits
2:00 - 3:30pm	Keynote Address: Hardening Legacy C/C++ Code (Abstract) Greg Morrisett (Harvard University School of Engineering and Applied Sciences)
3:30 - 4:00pm	Afternoon Break & Exhibits
4:00 - 5:30pm	Session: Advancing Compiler Technology The Implementation of Compile-Time Dimensionality Checking Vincent Pucci (AdaCore) and* Edmond Schonberg (AdaCore)* A robust implementation of Ada's finalizable controlled types Hristian Kirtchev (AdaCore)
5:30 - 6:30pm	Break
6:30 - 10:00pm	Evening Social Event Old Town Trolley tour and Legal Sea Foods dinner

Wednesday, December 5

TECHNICAL PROGRAM - Security and Safety

9:00 - 10:30am

Announcements

SIGAda Awards
John McCormick

Keynote Address:

HACMS: High-Assurance Vehicles
(Abstract)
Kathleen Fisher (DARPA Information Innovation Office)

10:30 - 11:00am

Morning Break and Exhibits

11:00am - 12:30pm

Session: Languages and Security

Formal Verification of the seL4 microkernel (Abstract)
Michael Norrish (NICTA (Australia))

DSL for Cross-Domain Security
D. S. Hardin (Rockwell Collins)

AdaCore Sponsor Presentation
Greg Gicca (AdaCore)

12:30 - 2:00pm

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

2:00 - 3:30pm

Keynote Address:

Challenges for Safety-Critical Software
(Abstract)
Nancy Leveson (Massachusetts Institute of Technology
Dept. of Aeronautics and Astronautics
Engineering Systems Division)

3:30 - 4:00pm

Afternoon Break

4:00 - 5:30pm

Session: Languages and Safety

Track 1: Industrial Session on Safety

Track 2: Real Time Systems

Real-Time Java in the Modernization of the Aegis Weapon System
Kelvin Nilsen (Atego, Inc.)

Software for FAA's Automatic Data Comm between Air Traffic Controller and Pilot
J. O'Leary (Federal Aviation Administration)

From the Model to the Target to Certification – Trends in growing use of code from model based development systems in high integrity environments (Abstract)
Jay Thomas (LDRA)

Synchronization cannot be a library
Geert Bosch (AdaCore)

Applicability of RT Schedulability Analysis on a Software Radio Protocol
Shuai Li (Lab-STICC/UMR), Frank Singhoff (University of Brest, France), Stéphane Rubini (Lab-STICC/UMR), and Michel Bourdellès (THALES Communications & Security)

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

5:30 - 8:00pm

Dinner Break

8:00 - 9:30pm

Session: Birds-of-a-Feather (BoF) and Workshops

Birds of a Feather: GNAT
Greg Gicca (AdaCore)

Thursday, December 6
TECHNICAL PROGRAM - Designing and Implementing Languages
9:00 - 10:30am	Announcements Best Paper and Student Paper Awards Jeff Boleng Keynote Address: Programming Language Life Cycles (Abstract) Guy Steele (Oracle Labs)
10:30 - 11:00am	Morning Break
11:00am - 1:00pm	Session: Compiler Certification Issues Adapting ACATS for Use with Run-Time Checks Suppressed Dan Eilers (Irvine Compiler Corp.) and* Tero Koskinen (Tampere, Finland)* Panel on Compiler Certification: Should You Trust Your Compiler? Tucker Taft (AdaCore), Lennart Beringer (Princeton University), Randy Brukardt (RR Software), and* Tom Plum (Plum Hall)* Ada-Europe'2013 Conference Announcement SIGAda 2013 Conference Announcement Alok Srivastava
1:00pm	Closing Comments & Conference Adjournment

Created on 4 December 2012; website comments and corrections to ClydeRoby at ACM.Org