Ben Brosgol, Jeff Boleng, S. Tucker Taft
Proceedings of the ACM Conference on High Integrity Language Technology
HILT, 2012.

@proceedings{HILT-2012,
	acmid         = "2402676",
	address       = "Boston, Massachusetts, USA",
	editor        = "Ben Brosgol and Jeff Boleng and S. Tucker Taft",
	isbn          = "978-1-4503-1505-0",
	publisher     = "{ACM}",
	title         = "{Proceedings of the ACM Conference on High Integrity Language Technology}",
	year          = 2012,
}

Contents (21 items)

4 ×#verification
3 ×#ada
3 ×#implementation
3 ×#named
3 ×#tutorial
3 ×#using
2 ×#automation
2 ×#bibliography
2 ×#compilation
2 ×#java

HILT-2012-Sanden #approach #design #modelling #multi

Design of Multitask Software: The Entity-life Modeling Approach (BIS), pp. 1–2.

HILT-2012-BeltCHR #ada #automation #contract #using #verification

Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.

HILT-2012-Kanig #ada #testing #verification

Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve — the hi-lite project (JK), pp. 5–6.

HILT-2012-LevesonFT #embedded #safety

Safety of embedded software (NGL, CHF, JT), pp. 7–8.

HILT-2012-Leino #source code

Developing verified programs with Dafny (KRML), pp. 9–10.

HILT-2012-SwardB #architecture #concept #implementation

Service-oriented architecture (SOA) concepts and implementations (RES, JB), pp. 11–12.

HILT-2012-Taft #divide and conquer #manycore #named #programming #tutorial #using

Tutorial: multicore programming using divide-and-conquer and work stealing (STT), pp. 13–14.

HILT-2012-Nilsen #comprehension #java #memory management #overview #safety #tutorial

Tutorial overview: understanding dynamic memory management in safety critical java (KN), pp. 15–22.

HILT-2012-Liskov #programming #turing machine

Keynote presentation: Programming the turing machine (BL), pp. 23–24.

HILT-2012-Leino12a #proving #using #verification #why

Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.

HILT-2012-KanigSD #compilation #convergence #named #verification

Hi-Lite: the convergence of compiler technology and program verification (JK, ES, CD), pp. 27–34.

HILT-2012-SchonbergP #ada #implementation

Implementation of a simple dimensionality checking system in Ada 2012 (ES, VP), pp. 35–42.

HILT-2012-Kirtchev #compilation #implementation #performance #robust

A new robust and efficient implementation of controlled types in the GNAT compiler (HHK), pp. 43–50.

HILT-2012-Fisher #assurance #named

HACMS: high assurance cyber military systems (KF), pp. 51–52.

HILT-2012-HardinSWP #domain-specific language #security

A DSL for cross-domain security (DSH, KS, MWW, THP), pp. 53–62.

HILT-2012-Nilsen12a #java #legacy #realtime

Real-time Java in modernization of the aegis weapon system (KN), pp. 63–70.

HILT-2012-OLearyS #automation #communication #development

FAA’s controller pilot automatic data communication (data comm) system software development (JO, AS), pp. 71–72.

HILT-2012-Bosch #library

Synchronization cannot be implemented as a library (GB), pp. 73–80.

HILT-2012-LiSRM #analysis #protocol #realtime #scheduling

Applicability of real-time schedulability analysis on a software radio protocol (SL, FS, SR, MB), pp. 81–94.

HILT-2012-Steele #lifecycle #programming language

Programming language life cycles (GLSJ), pp. 95–96.

HILT-2012-EilersK #adaptation #runtime

Adapting ACATS for use with run-time checks suppressed (DE, TK), pp. 97–102.