Jeff Boleng, S. Tucker Taft
Proceedings of the ACM SIGAda Annual Conference on High Integrity Language Technology
HILT, 2013.

@proceedings{HILT-2013,
	address       = "Pittsburgh, Pennsylvania, USA",
	doi           = "10.1145/2527269",
	editor        = "Jeff Boleng and S. Tucker Taft",
	isbn          = "978-1-4503-2467-0",
	publisher     = "{ACM}",
	title         = "{Proceedings of the ACM SIGAda Annual Conference on High Integrity Language Technology}",
	year          = 2013,
}

Contents (20 items)

4 ×#verification
3 ×#development
3 ×#formal method
3 ×#modelling
3 ×#named
3 ×#using
2 ×#analysis
2 ×#architecture
2 ×#contract
2 ×#parallel

HILT-2013-Taft #concurrent #named #parallel #proving #safety #source code #thread #tutorial

Tutorial: proving safety of parallel / multi-threaded programs (STT), pp. 1–2.

HILT-2013-Jackson #domain-specific language

Engineering domain-specific languages with formula 2.0 (EKJ), pp. 3–4.

HILT-2013-Bjorner #development #modulo theories #satisfiability

Satisfiability modulo theories for high integrity development (NB), pp. 5–6.

HILT-2013-Logozzo #contract #specification #verification

Practical specification and verification with code contracts (FL), pp. 7–8.

HILT-2013-Chaki #bound #model checking

Bounded model checking of high-integrity software (SC), pp. 9–10.

HILT-2013-BolengS #architecture #concept #implementation

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

HILT-2013-Logozzo13a #contract

Technology for inferring contracts from code (FL), pp. 13–14.

HILT-2013-CarterFHHT #analysis #named

SAW: the software analysis workbench (KC, AF, JH, BH, AT), pp. 15–18.

HILT-2013-EfstathopoulosH #optimisation #verification

Optimizing verification effort with SPARK 2014 (PE, AH), pp. 19–20.

HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.

HILT-2013-MichellMP #manycore #programming #realtime

Real-time programming on accelerator many-core processors (SM, BM, LMP), pp. 23–36.

HILT-2013-Taft13a #ada #parallel #programming #set

Bringing safe, dynamic parallel programming to the spark verifiable subset of ada (STT), pp. 37–40.

HILT-2013-Whalen #analysis #architecture #development #formal method #modelling #scalability #using

Up and out: scaling formal analysis using model-based development and architecture modeling (MWW), pp. 41–42.

HILT-2013-WardRL #approach #integration #process

An approach to integration of complex systems: the SAVI virtual integration process (DTW, DAR, BAL), pp. 43–46.

HILT-2013-DoranA #development #embedded #modelling #named #tool support

Reddo: a model driven engineering toolset for embedded software development (SD, SEA), pp. 47–48.

HILT-2013-Goodenough #behaviour

Building confidence in system behavior (JBG), pp. 49–50.

HILT-2013-MurugesanWRH #composition #verification

Compositional verification of a medical device system (AM, MWW, SR, MPEH), pp. 51–64.

HILT-2013-LarsonHFD #fault #modelling #safety #using

Illustrating the AADL error modeling annex (v.2) using a simple safety-critical medical device (BRL, JH, KF, JD), pp. 65–84.

HILT-2013-Wing #formal method #industrial #perspective

Formal methods: an industrial perspective (JMW), pp. 85–86.

HILT-2013-Alagic #automation #interactive #verification

Automatic versus interactive program verification (SA), pp. 87–88.