HILT 2012             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, December 2
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
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
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
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


SIGAda Awards
John McCormick

Keynote Address:

HACMS: High-Assurance Vehicles
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
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


Best Paper and Student Paper Awards
Jeff Boleng

Keynote Address:

Programming Language Life Cycles
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