Login / Signup
HILT
2012
2014
2012
2014
Keyphrases
Publications
2014
Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014
HILT
(2014)
Thomas Ball
Correctness via compilation to logic: a decade of verification at microsoft research.
HILT
(2014)
Robert Bocchino
,
Nicholas Matsakis
,
S. Tucker Taft
,
Brian Larson
,
Ed Seidewitz
Panel summary: finding safety in numbers: new languages for safe multicore programming and modeling.
HILT
(2014)
Peter H. Feiler
AADL and model-based engineering.
HILT
(2014)
Christine Anderson
From Ada 9x to spaceport America: going where no one has gone before.
HILT
(2014)
S. Tucker Taft
,
Brad Moore
,
Luís Miguel Pinho
,
Stephen Michell
Safe parallel programming in ada with language extensions.
HILT
(2014)
William Rathje
,
Brad Richards
A framework for model checking UDP network programs with Java pathfinder.
HILT
(2014)
Ed Seidewitz
UML with meaning: executable modeling in foundational UML and the Alf action language.
HILT
(2014)
David Crocker
Can C++ be made as safe as SPARK?
HILT
(2014)
Nicholas D. Matsakis
,
Felix S. Klock II
The rust language.
HILT
(2014)
Jérôme Hugues
,
Christophe Garion
Leveraging Ada 2012 and SPARK 2014 for assessing generated code from AADL models.
HILT
(2014)
Robert L. Bocchino
,
Edward B. Gamble
,
Kim P. Gostelow
,
Raphael R. Some
Spot: a programming language for verified flight software.
HILT
(2014)
Anya Helene Bagge
,
Magne Haveraaen
Specification of generic APIs, or: why algebraic may be better than pre/post.
HILT
(2014)
Tamás Szabó
,
Markus Voelter
,
Bernd Kolb
,
Daniel Ratiu
,
Bernhard Schätz
mbeddr: extensible languages for embedded software development.
HILT
(2014)
Brian R. Larson
Formal semantics for the PACEMAKER system specification.
HILT
(2014)
Ehsan Ahmad
,
Brian R. Larson
,
Stephen C. Barrett
,
Naijun Zhan
,
Yunwei Dong
Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling.
HILT
(2014)
John Barnes
,
S. Tucker Taft
Ada 83 to Ada 2012: lessons learned over 30 years of language design.
HILT
(2014)
Andrew Gacek
,
John Backes
,
Darren D. Cofer
,
Konrad Slind
,
Mike Whalen
Resolute: an assurance case language for architecture models.
HILT
(2014)
2013
Pierre Courtieu
,
Maria-Virginia Aponte
,
Tristan Crolard
,
Zhi Zhang
,
Robby
,
Jason Belt
,
John Hatcliff
,
Jérôme Guitton
,
Trevor Jennings
Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq.
HILT
(2013)
Ethan K. Jackson
Engineering domain-specific languages with formula 2.0.
HILT
(2013)
Francesco Logozzo
Practical specification and verification with code contracts.
HILT
(2013)
S. Tucker Taft
Tutorial: proving safety of parallel / multi-threaded programs.
HILT
(2013)
Suad Alagic
Automatic versus interactive program verification.
HILT
(2013)
Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, HILT 2013, Pittsburgh, Pennsylvania, USA, November 10-14, 2013
HILT
(2013)
Brian R. Larson
,
John Hatcliff
,
Kim R. Fowler
,
Julien Delange
Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device.
HILT
(2013)
Steven Doran
,
Stephanie E. August
Reddo: a model driven engineering toolset for embedded software development.
HILT
(2013)
Jeff Boleng
,
Ricky E. Sward
Service-oriented architecture (SOA) concepts and implementations.
HILT
(2013)
S. Tucker Taft
Bringing safe, dynamic parallel programming to the spark verifiable subset of ada.
HILT
(2013)
Francesco Logozzo
Technology for inferring contracts from code.
HILT
(2013)
Pavlos Efstathopoulos
,
Andrew Hawthorn
Optimizing verification effort with SPARK 2014.
HILT
(2013)
Sagar Chaki
Bounded model checking of high-integrity software.
HILT
(2013)
Michael W. Whalen
Up and out: scaling formal analysis using model-based development and architecture modeling.
HILT
(2013)
Donald T. Ward
,
David A. Redman
,
Bruce A. Lewis
An approach to integration of complex systems: the SAVI virtual integration process.
HILT
(2013)
John B. Goodenough
Building confidence in system behavior.
HILT
(2013)
Nikolaj Bjørner
Satisfiability modulo theories for high integrity development.
HILT
(2013)
Jeannette M. Wing
Formal methods: an industrial perspective.
HILT
(2013)
Stephen Michell
,
Brad Moore
,
Luís Miguel Pinho
Real-time programming on accelerator many-core processors.
HILT
(2013)
Kyle Carter
,
Adam Foltzer
,
Joe Hendrix
,
Brian Huffman
,
Aaron Tomb
SAW: the software analysis workbench.
HILT
(2013)
Anitha Murugesan
,
Michael W. Whalen
,
Sanjai Rayadurgam
,
Mats Per Erik Heimdahl
Compositional verification of a medical device system.
HILT
(2013)
2012
Johannes Kanig
Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve - the hi-lite project.
HILT
(2012)
Lennart Beringer
,
Randall Brukardt
,
Thomas Plum
,
S. Tucker Taft
Panel on compiler certification: should we trust our compiler?
HILT
(2012)
K. Rustan M. Leino
Developing verified programs with Dafny.
HILT
(2012)
Bo Ingvar Sandén
Hilt'12 tutorial overview / design of multitask software: the entity-life modeling approach.
HILT
(2012)
Ricky E. Sward
,
Jeff Boleng
Service-oriented architecture (SOA) concepts and implementations.
HILT
(2012)
David S. Hardin
,
Konrad Slind
,
Michael W. Whalen
,
Tuan-Hung Pham
A DSL for cross-domain security.
HILT
(2012)
Shuai Li
,
Frank Singhoff
,
Stéphane Rubini
,
Michel Bourdellès
Applicability of real-time schedulability analysis on a software radio protocol.
HILT
(2012)
Johannes Kanig
,
Edmond Schonberg
,
Claire Dross
Hi-Lite: the convergence of compiler technology and program verification.
HILT
(2012)
Edmond Schonberg
,
Vincent Pucci
Implementation of a simple dimensionality checking system in Ada 2012.
HILT
(2012)
S. Tucker Taft
Tutorial: multicore programming using divide-and-conquer and work stealing.
HILT
(2012)
Geert Bosch
Synchronization cannot be implemented as a library.
HILT
(2012)