CINXE.COM

<!DOCTYPE html> <html> <head> <meta name="viewport" content="width=device-width, initial-scale=1, maximum-scale=1"> <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> <link href="https://conf.researchr.org/favicon.ico?28d37e6d7e5e12d24c39bdba0f4f3cfd" rel="shortcut icon" type="image/x-icon" /> <link href="https://conf.researchr.org/stylesheets/common_.css?d7bcca3579a066193caf560ede9d6399" rel="stylesheet" type="text/css" /> <title>ASE 2022 - [Workshop] HILT' 22 -- Supporting a Rigorous Approach to Software Development - ASE 2022</title> <script type="text/javascript">var show_webdsl_debug=false;</script> <script type="text/javascript">var contextpath="https://conf.researchr.org";</script> <link rel="stylesheet" href="https://conf.researchr.org/stylesheets/bootstrap/css/bootstrap.min.css?7f89537eaf606bff49f5cc1a7c24dbca" type="text/css" /><link rel="stylesheet" href="https://conf.researchr.org/stylesheets/conf.css?e0c92ee5f52769e04d268b7588469bfe" type="text/css" /><link rel="stylesheet" href="https://conf.researchr.org/getFile/d91b28e5-9960-4ab7-b4ef-598fc8d51056/ase-2022.css?1659796234904" type="text/css" /><link rel="stylesheet" href="https://conf.researchr.org/stylesheets/flatpickr-4.3.2.min.css?8eedb7a0f2455c0dbbbbcc46c4172c0d" type="text/css" /><link rel="stylesheet" href="https://conf.researchr.org/stylesheets/theme.bootstrap_3.min.css?6867e70881e6ed2c03b6c9cf9c3152e0" type="text/css" /><script type="text/javascript" src="//code.jquery.com/jquery-3.5.1.min.js"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/faceted-filtering.js?b66007ca48ecd1d87e1cdd60e4e42366"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/flatpickr-4.3.2.min.js?c2885c17ae5fd471c9a40c437e8a2736"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/jquery.tablesorter.combined.min.js?285b21976326641f8f1b910492e6d5d0"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/jquery.tablesorter.pager.min.js?4551cdfea66f45a11ae5548f3d50a06f"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/tablesorter-init.js?ee6babedf1a6be960e4543a1bb57b421"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/bootstrap/js/bootstrap.min.js?2f34b630ffe30ba2ff2b91e3f3c322a1"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/notify.min.js?e86d399917a84b69a4683f504c7a7813"></script> <script type="text/javascript" src="https://conf.researchr.org/javascript/ajax.js?2dbd1cc4f8f2d52ae9c879d7346f4f8a"></script> <script type="text/javascript">(function($){ $(document).ready(function(){ $('ul.dropdown-menu [data-toggle=dropdown]').on('click', function(event) { event.preventDefault(); event.stopPropagation(); $(this).parent().siblings().removeClass('open'); $(this).parent().toggleClass('open'); }); }); })(jQuery); </script> <script type="text/javascript"> $(window).on('popstate', function(){ $('.modal.in').modal('hide') }); </script><script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; $(node).find('.modal').on( 'shown.bs.modal', function(){ if(history.pushState){ history.pushState({ id: 'modal', modalId: $(this).attr('id') }, null, window.location.href); } } ).on( 'hidden.bs.modal', function (){ if( history.state != null && history.state.modalId == $(this).attr('id') ){ history.back(); } } ); }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script> <script>window.dataLayer = window.dataLayer || [];function gtag(){dataLayer.push(arguments);}gtag('js', new Date());gtag('config', 'G-4G0QWEKVQS', {'cookie_domain': 'auto', 'anonymizeIp': true });gtag('config', 'UA-9607501-2', {'cookie_domain': 'auto', 'anonymizeIp': true });</script> <script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; $(node).find('input.flatpickr:not([id])').focusout( function(){ this.dispatchEvent( new KeyboardEvent('keydown',{keyCode:13, bubbles: true}) ); } ); }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script> <script type="text/javascript">var ignoreHashChange = false; function hashChangeFunc(){ // show active tab on hash in url if (window.location.hash !== ''){ var hashTargetAll = $('a[href="' + window.location.hash + '"]'); if(hashTargetAll.length){ var hashTarget = hashTargetAll.filter('[data-toggle="tab"]') if( hashTarget.length ){ hashTarget = hashTarget.first(); hashTarget.tab('show'); } else { hashTarget = hashTargetAll.first(); } // and open parent tabs in case the target element is nested in a tab var parentPane = hashTarget.closest( '.tab-pane' ); if(parentPane.length){ $('.nav a[href="#'+ parentPane.attr('id') +'"]').tab('show'); } var parentCollapse = hashTarget.closest( '.panel-collapse:not(.in)' ).collapse('show'); } } return false; } $(document).ready(function(){ var tabFromRequestUrl = window.location.hash !== '' ? $('a[href="' + window.location.hash + '"][data-toggle="tab"]') : []; var initUrlHash = window.location.hash; hashChangeFunc() if( tabFromRequestUrl.length ){ //Prevent the browser to auto-scroll to the anchor of the tab window.location.hash = ""; } //make in-page #links open the tabs if ($._data( $(window)[0], 'events' ).hashchange == undefined){ $(window).on('hashchange', hashChangeFunc); } if(tabFromRequestUrl.length){ setTimeout( function(){ ignoreHashChange = true; history.replaceState(null, null, initUrlHash); ignoreHashChange = false; }, 10 ); } }); var autoTabFunction = function(node){ // remember the hash in the URL without jumping $('a[data-toggle="tab"]:not(.no-hash):not(.bound)').addClass('bound').on('shown.bs.tab', function(e){ var newhash = '#' + $(e.target).attr('href').substr(1); if(history.replaceState){ history.replaceState(null, null, newhash); } else{ location.hash = newhash; } }); //When no tab is active, set the first one to active $(node).find('.nav-tabs:not(.bound), .nav-pills:not(.bound)').addClass('bound').each(function(){ if( $(this).children().length > 0 && 1 > $(this).find('.active').length){ $(this).children().first().addClass('active'); } }); $(node).find('.tab-content:not(.bound)').addClass('bound').each(function(){ if( $(this).children().length > 0 && 1 > $(this).children('.active').length){ $(this).children('.tab-pane').first().addClass('active'); } }); } </script> <script type="text/javascript">function addEventModalLoadOnClick( containerNode ){ $(containerNode).find( "a[data-event-modal]" ).on("click", function(e){ var eventId = $(this).data("event-modal"); var modalElem = $("#modal-" + eventId); if(modalElem.length){ modalElem.modal({ backdrop: 'static', keyboard: true}, 'show'); } else { var loaderElem = $("#event-modal-loader"); loaderElem.find("input.event-id-input").val( eventId ); loaderElem.find("#load-modal-action").click(); } e.preventDefault(); } ); } </script><script type="text/javascript">function addStarredEventOnClick( containerNode ){ $(containerNode).find( "[data-event-star]" ).on("click", function(e){ var eventId = $(this).data("event-star"); var starEventFormElem = $("#event-star-form"); starEventFormElem.find("input.event-id-input").val( eventId ); starEventFormElem.find("#star-event-action").click(); e.preventDefault(); e.stopPropagation(); } ); } </script><script type="text/javascript">function pauseOnCloseModal( modalid ){ //pauses video (only youtube at the moment) when closing modal $('#' + modalid).on('hidden.bs.modal', function () { $(this).find('.embed-container iframe[src*=enablejsapi]').each( function(){ this.contentWindow.postMessage('{"event":"command","func":"pauseVideo","args":""}', '*') } ); } ) } </script> <meta prefix='og: http://ogp.me/ns#' property='og:image' content='https://conf.researchr.org/getImage/ase-2022/carousel/About_UCM-19838_002.jpg?1658910969000'> <meta name='description' content='This is the seventh in the HILT series of conferences and workshops focused on the use of High Integrity Language Technology to address challenging issues in the engineering of highly complex critical software systems. HILT is organized by ACM SigAda, in cooperation with Ada Europe. High Integrity Language Technologies have been tackling the challenges of building efficient, safe, reliable software for decades. Critical software as a domain is quickly expanding beyond embedded real-time control applications to the increasing reliance on complex software for the basic functioning of busine ...'> <script type="text/javascript">$(document).ready( function(){ $('#program-menu a[data-fltr-type]').on('click', function(event){ event.preventDefault(); window.location = $(this).attr('href') + "?" + encodeURIComponent( $(this).data('fltr-type') ) + '=' + encodeURIComponent( $(this).data('fltr-val') ); }) }) </script> <script async src="https://www.googletagmanager.com/gtag/js?id=G-4G0QWEKVQS"></script> <meta prefix='og: http://ogp.me/ns#' property='og:title' content='ASE 2022 - [Workshop] HILT' 22 -- Supporting a Rigorous Approach to Software Development - ASE 2022'>  <meta prefix='og: http://ogp.me/ns#' property='og:description' content='This is the seventh in the HILT series of conferences and workshops focused on the use of High Integrity Language Technology to address challenging issues in the engineering of highly complex critical software systems. HILT is organized by ACM SigAda, in cooperation with Ada Europe. High Integrity Language Technologies have been tackling the challenges of building efficient, safe, reliable software for decades. Critical software as a domain is quickly expanding beyond embedded real-time control applications to the increasing reliance on complex software for the basic functioning of busine ...'> </head> <body id="track"><div class="frame"><a href="https://conf.researchr.org/blogposts/ase-2022" class="blog-link btn btn-xs btn-default navigate">Write a Blog >></a><div class="logobar"><div class="container"><a href="https://conf.researchr.org/home/ase-2022" class="navbar-brand navigate"><span class="brand-text">ASE 2022</span></a><div class="place">Mon 10 - Fri 14 October 2022 <a href="https://conf.researchr.org/venue/ase-2022/ase-2022-venue" class="navigate">Oakland Center, Michigan, United States</a></div></div></div><div class="navbar navbar-default"><div class="container"><div class="navbar-header"><button type="button" data-toggle="collapse" data-target="#navigationbar" class="navbar-toggle"><span class="sr-only">Toggle navigation</span><span class="icon-bar"></span><span class="icon-bar"></span><span class="icon-bar"></span></button></div><div id="navigationbar" class="navigationbar collapse navbar-collapse"><ul class="block nav navbar-nav"><li class="dropdown"><a href="#" data-toggle="dropdown" class="dropdown-toggle">Attending <span class="caret"></span></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/venue/ase-2022/ase-2022-venue" class="navigate">Venue: Oakland Center, Michigan, USA</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/attendee-information" class="navigate">Attendee Information</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/presenter-information" class="navigate">Presenter Information</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/covid-19-protocol" class="navigate">COVID-19 Protocol</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/registration" class="navigate">Registration</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/accommodation" class="navigate">Accommodation</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/visa-letters" class="navigate">Visa Letters</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/travel-support" class="navigate">Travel Support</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/diversity-and-inclusion" class="navigate">Diversity and Inclusion</a></li><li class="block"><a href="https://conf.researchr.org/attending/ase-2022/code-of-conduct" class="navigate">Code of Conduct</a></li></ul></li><li class="block"><a href="https://conf.researchr.org/info/ase-2022/sponsorship-opportunities" class="navigate">Sponsorship Opportunities</a></li><li class="dropdown"><a href="#" data-toggle="dropdown" class="dropdown-toggle">Program <span class="caret"></span></a><ul id="program-menu" class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" class="navigate">ASE Program</a></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="prog" data-fltr-val="Your Program" class="navigate"><span class="glyphicon glyphicon-star"></span> Your Program</a></li><li class="block"><a href="https://conf.researchr.org/info/ase-2022/keynotes" class="navigate">Keynotes</a></li><li class="block"><a href="https://conf.researchr.org/info/ase-2022/week-overview" class="navigate">Week Overview</a></li><li class="block"><a href="https://conf.researchr.org/info/ase-2022/social-events" class="navigate">Social Events</a></li><li class="block"><a href="https://conf.researchr.org/info/ase-2022/awards" class="navigate">Awards</a></li><li class="block divider"></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="date" data-fltr-val="Mon 10 Oct 2022" class="navigate">Mon 10 Oct</a></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="date" data-fltr-val="Tue 11 Oct 2022" class="navigate">Tue 11 Oct</a></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="date" data-fltr-val="Wed 12 Oct 2022" class="navigate">Wed 12 Oct</a></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="date" data-fltr-val="Thu 13 Oct 2022" class="navigate">Thu 13 Oct</a></li><li class="block"><a href="https://conf.researchr.org/program/ase-2022/program-ase-2022/" data-fltr-type="date" data-fltr-val="Fri 14 Oct 2022" class="navigate">Fri 14 Oct</a></li></ul></li><li id="tracks-in-navbar" class="dropdown"><a href="#" data-toggle="dropdown" class="dropdown-toggle">Tracks <span class="caret"></span></a><ul class="block dropdown-menu multi-column columns-1"><div class="row"><div class="col-sm-12"><ul class="block multi-column-dropdown"><li class="block dropdown-header">ASE 2022</li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-artifact-evaluation" class="navigate">Artifact Evaluation</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-doctoral-symposium" class="navigate">Doctoral Symposium</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-industry-showcase" class="navigate">Industry Showcase</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-journal-first-papers" class="navigate">Journal-first Papers</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-late-breaking-results" class="navigate">Late Breaking Results</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-nier-track" class="navigate">NIER Track</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-research-papers" class="navigate">Research Papers</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-student-research-competition" class="navigate">Student Research Competition</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-student-volunteers" class="navigate">Student Volunteers</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-tool-demonstrations" class="navigate">Tool Demonstrations</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-tutorials" class="navigate">Tutorials</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshops" class="navigate">Workshops</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-a-mobile-22" class="navigate">[Workshop] A-Mobile '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-ase4games-22" class="navigate">[Workshop] ASE4Games '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-aust-22" class="navigate">[Workshop] AUST '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-aesir-22" class="navigate">[Workshop] AeSIR '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hcse-cs-22" class="navigate">[Workshop] HCSE&CS '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" class="navigate">[Workshop] HILT' 22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-iwor-22" class="navigate">[Workshop] IWoR '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-jpf-22" class="navigate">[Workshop] JPF '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-varse-22" class="navigate">[Workshop] VARSE '22</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-diversity-and-inclusion-events" class="navigate">Diversity and Inclusion Events</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-meetings" class="navigate">Meetings</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-plenary" class="navigate">Plenary</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-mip-awards" class="navigate">MIP Awards</a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-posters-" class="navigate">Posters </a></li><li class="block"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-keynotes" class="navigate">Keynotes</a></li></ul></div></div></ul></li><li class="dropdown"><a href="#" data-toggle="dropdown" class="dropdown-toggle">Organization <span class="caret"></span></a><ul class="block dropdown-menu multi-column columns-1"><div class="row"><div class="col-sm-12"><ul class="block multi-column-dropdown"><li class="block dropdown-header">ASE 2022 Committees</li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-organizing-committee" class="navigate">Organizing Committee</a></li><li class="block dropdown-header">Track Committees </li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Artifact Evaluation</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-artifact-evaluation-artifact-evaluation-chairs" class="navigate">Artifact Evaluation Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-artifact-evaluation-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Doctoral Symposium</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-doctoral-symposium-doctoral-symposium-chairs" class="navigate">Doctoral Symposium Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-doctoral-symposium-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Industry Showcase</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-industry-showcase-industry-showcase-chairs" class="navigate">Industry Showcase Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-industry-showcase-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Journal-first Papers</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/journal-first-papers-chairs" class="navigate">Journal-first Papers Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-journal-first-papers-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Late Breaking Results</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-late-breaking-results-late-breaking-results-chairs" class="navigate">Late Breaking Results Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-late-breaking-results-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>NIER Track</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-nier-track-nier-track-chairs" class="navigate">NIER Track Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-nier-track-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Research Papers</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-research-papers-research-papers-chair" class="navigate">Research Papers Chair</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-research-papers-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Student Research Competition</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-student-research-competition-student-research-competition-chairs" class="navigate">Student Research Competition Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-student-research-competition-judges" class="navigate">Judges</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-student-research-competition-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-student-volunteers-student-volunteers-chairs" class="navigate"><strong>Student Volunteers</strong></a></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Tool Demonstrations</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-tool-demonstrations-tool-demonstrations-chair" class="navigate">Tool Demonstrations Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-tool-demonstrations-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="dropdown dropdown-submenu "><a href="#" data-toggle="dropdown" class="dropdown-toggle"><strong>Tutorials</strong></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-tutorials-tutorials-chairs" class="navigate">Tutorials Chairs</a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-tutorials-program-committee" class="navigate">Program Committee</a></li></ul></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-workshops-workshops-chairs" class="navigate"><strong>Workshops</strong></a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-diversity-and-inclusion-events-diversity-chairs" class="navigate"><strong>Diversity and Inclusion Events</strong></a></li><li class="block"><a href="https://conf.researchr.org/committee/ase-2022/ase-2022-mip-awards-mip-co-chairs" class="navigate"><strong>MIP Awards</strong></a></li><li class="block dropdown-header">Contributors</li><li class="block"><a href="https://conf.researchr.org/people-index/ase-2022" class="navigate"><span class="glyphicon glyphicon-search"></span><sup><span class="glyphicon glyphicon-user"></span></sup> People Index</a></li></ul></div></div></ul></li><li class="block"><a href="https://conf.researchr.org/search/ase-2022//all" class="navigate"><span class="glyphicon glyphicon-search"></span><span class="hidden-sm"> Search</span></a></li><li class="dropdown"><a href="#" data-toggle="dropdown" class="dropdown-toggle"><span class="hidden-sm">Series <span class="caret"></span></span><span title="Series" class="visible-sm"><span class="glyphicon glyphicon-repeat"></span> <span class="caret"></span></span></a><ul class="block dropdown-menu"><li class="block"><a href="https://conf.researchr.org/series/ase" class="navigate"><span class="glyphicon glyphicon-home"></span> Series</a></li><li class="block divider"></li><li class="block"></li><li class="block"><a href="https://conf.researchr.org/home/ase-2025" class="navigate">ASE 2025</a></li><li class="block"><a href="https://conf.researchr.org/home/ase-2024" class="navigate">ASE 2024</a></li><li class="block"><a href="https://conf.researchr.org/home/ase-2023" class="navigate">ASE 2023</a></li><li class="block"><span class="text-muted" style="margin-left: 2px;"><span class="glyphicon glyphicon-hand-right"></span> ASE 2022</span></li><li class="block"><a href="https://conf.researchr.org/home/ase-2021" class="navigate">ASE 2021</a></li><li class="block"><a href="https://conf.researchr.org/home/ase-2020" class="navigate">ASE 2020</a></li><li class="block"><a href="https://2019.ase-conferences.org" class="navigate">ASE 2019</a></li><li class="block"><a href="http://ase-conferences.org/ase/past/index.html" target="_blank" class="navigate">Past Editions <span class="pull-right"><span class="glyphicon glyphicon-new-window"></span></span></a></li></ul></li></ul><div class="navbar-right"><ul class="block nav navbar-nav"><li class="block"><a href="https://conf.researchr.org/signin/ase-2022/https%3A%5Es%5Esconf.researchr.org%5Estrack%5Esase-2022%5Esase-2022-workshop-hilt-22" rel="nofollow" class="navigate">Sign in</a></li><li class="block"><a href="https://conf.researchr.org/signup/ase-2022" class="navigate">Sign up</a></li></ul></div></div></div></div><div id="content" class="container"><div class="page-header"><span class="text-muted small"><span class="glyphicon glyphicon-home"></span> <a href="https://conf.researchr.org/home/ase-2022" class="navigate">ASE 2022</a> (<a href="https://conf.researchr.org/series/ase" class="navigate">series</a>) / </span><h1>[Workshop] HILT' 22 -- Supporting a Rigorous Approach to Software Development<span class="pull-right small h1">ASE 2022</span></h1></div><div class="row"><div class="col-sm-12"><ul id="tab" class="nav nav-pills"><li><a href="#About" data-toggle="tab">About</a></li><li><a href="#program" data-toggle="tab">Program</a></li></ul><script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; autoTabFunction(node); }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script><div class="tab-content"><div id="About" class="tab-pane "><p>This is the seventh in the HILT series of conferences and workshops focused on the use of High Integrity Language Technology to address challenging issues in the engineering of highly complex critical software systems. HILT is organized by <a href="http://sigada.org/">ACM SigAda</a>, in cooperation with <a href="https://www.ada-europe.org/">Ada Europe</a>.</p> <p>High Integrity Language Technologies have been tackling the challenges of building efficient, safe, reliable software for decades. Critical software as a domain is quickly expanding beyond embedded real-time control applications to the increasing reliance on complex software for the basic functioning of businesses, governments, and society in general.</p> <p>For its 2022 edition, HILT will be a workshop of the 37th IEEE/ACM International Conference on Automated Software Engineering, <a href="https://conf.researchr.org/home/ase-2022">ASE’2022</a>. The workshop will be held on October 14<sup>th</sup> 2022.</p> <p>See <a href="https://conf.researchr.org/home/ase-2022">ASE’2022</a> for details on the venue and registration.</p> <h2><a href="#keynotes" id="keynotes" class="anchor-link">Keynotes</a></h2> <center><strong>The keynote speakers for HILT 2022 are two leaders in their field:</strong><br><br></center> <table style="margin-left:auto; margin-right:auto"> <tbody><tr> <td><center><img src="http://www.mathmeth.com/leino/images/index.jpg" alt="K. Rustan M. Leino" height="300" width="200"></center></td> <td>            </td> <td><center><img src="https://avatars.githubusercontent.com/u/155238?v=4" alt="Niko Matsakis" height="300" width="300"></center></td> </tr> <tr> <td><center>K. Rustan M. Leino: <br><strong><i> Recent experience with developing<br>formally verified software</i></strong></center></td> <td> </td> <td><center>Niko Matsakis: <br>  <strong><i>a-mir-formality:</i> <br>a formal model for the Rust language</strong>  </center></td> </tr> </tbody></table> <h2><a href="#topics" id="topics" class="anchor-link">Topics</a></h2> <p>HILT 2022 will focus on the increasing synergies between formal methods (theorem provers, SAT, SMT, etc.), advanced static analysis (model checking, abstract interpretation), software design and modeling, and safety-oriented languages. From separate fields of research, we now observe a stronger interconnection between formal methods, advanced analytics, modeling and design of software, and safety features in programming languages. Programming languages for safety-critical systems now routinely integrate theorem proving capabilities like C/ACSL or Ada/SPARK2014. Theorem provers such as Coq, Lean, or Isabelle have established themselves as a viable strategy to implement compilers or properly define the semantics of domain-specific languages. Tools for verifying modeling languages such as AADL, Lustre, and Simulink are becoming more widely available, and with the emergence of the Rust language and the release of Ada 2022, safety is rising to the top of concerns for critical systems developers.</p> <p>The HILT’2022 workshop seeks to explore ways High Integrity Language Technologies leverage recent advances in practical formal methods and language design to deliver the next generation of safety-critical systems.</p> <h2><a href="#sponsor" id="sponsor" class="anchor-link">Sponsor</a></h2> <p>The organizers of the HILT 2022 workshop wish to thank this year’s sponsor: <a href="https://www.adacore.com"> <img src="https://lh3.googleusercontent.com/a829bMSnB9KLqpBIna8Qhp53fiLKkBejgS9wwLGdTaAhPKMSIF1KbKrY5KVqWiHkKKPt8lBbL2Bv9j6_AFjREaLy9E4xsNPwjrnTKses7ibVefYM99-4-OB6uizTgj9cTT3TsWxXmpAGOKlbTH4Mz7E0XH5ygK-a7rfKF2NrnSn9IpVGHx71nP61ezzgNyWd0Ch-FPt3De3x0dMXafpuDg7I4hsaWg62StQZH-92d4ZxVm2zLA_aXk9huJCwJ4FWuqtnpJe7YJWkZzT8WkGMjepzL_uTZ_8jxt1qbtr7f1HKQzTnOSGUv96AfoVduQ66nNWqeS5Vpy80flgyW7PCE62fp_rAC9MElUPgQaX8iOz-YQnbqBe7D3JlAS7PTWBteIxJMxLEkJ-DP1kCU2-sYCc_jcL_iRE6je7gThcQbi_B2fciNFigbqEWqYvl8zLwLDGJFRR4xc9B6LSsJrl1gOD5fUV6vBiCdu-9xjPIA0AxKlm8U1T0z992UBnhW7r-94cSN1wHYCiv_4LDYdZwzLuJfM9_YkoAe25lXuVm_Dc5FwyZBiJNx9WVnPG2_BEfSInu3depNfYCXsixd4Gq2KscBJS0o0cAnaE0xkKoBqMXgruz_c9PT2AWz80ZyhHJw9C0Ey578skREjkCPNKv3FcKTVlDOmOeUOkcQVbZPn_A9yscPKOwO2a1VFkogWrFuEsbSA1isQ8LdbHHbQMg28oVIf67-19SHX_eLkMjOzdx7aK7tt-S3xpIcn2eqdXAyRK_SmKCkyDqIR8c_uIOxobCY3CPflsi86n59dMc6BsdnW69_RKNJaGnYkAN7I-XnbjJ632s390P8_hSuEI4qoIhUV_WcT48CvN1b-ni61W_GG1S90E8hNMXQtCJphEh-aV_EfQvlGre4hJLQoeWFWG2tcTclud_bKH8dh6MV9SxOtLJMVgT5uVkKbhSphWDY19eZaa9ITuxyRWXrDIcWSaarr0sVzO-XwjU0vbVY-q-PM_G=w2116-h446-no?authuser=0" alt="AdaCore" height="30" width="150"></a></p> </div><div id="program" class="tab-pane "><div class="faceted-filtering"><div class="row plenary-facets"><div class="col-sm-1"><strong>Plenary</strong></div><div class="col-sm-11"><div data-facet-type="plenary" class="facet-placeholder"></div></div></div><script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; $(node).find('.modal').on('shown.bs.modal', function() {if(gtag) { gtag( 'event', 'Show Details in Modal' , {'event_category': 'Event Information', 'event_label': '' + $(this).find('.modal-title').text() + ''} ) } } ) }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script><div tabindex="-1" id="hidden-modal" class="modal"><div class="modal-dialog "><div class="modal-content"></div></div></div><div id="program-settings-modal" class="webdsl-placeholder"><div id="userProgramSettings" class="modal fade"><div class="modal-dialog "><div class="modal-content"><div class="modal-header"><a data-dismiss="modal" class="close"><span class="glyphicon glyphicon-remove"></span></a><h3>Program Display Configuration</h3></div><div class="modal-body"><form name="form11390898770538530f0e2bbdb67872b491120c5c8a7" id="form11390898770538530f0e2bbdb67872b491120c5c8a7" action="https://conf.researchr.org/userProgramSettingsModalConferenceEdition" accept-charset="UTF-8" method="POST" role="form" class="form-horizontal"><input type="hidden" name="form11390898770538530f0e2bbdb67872b491120c5c8a7" value="1" /><input type="hidden" name="context" value="ase-2022" /><div class="panel panel-default timezone-panel"><div class="panel-heading clearfix"><div class="panel-title">Time Zone</div></div><div class="panel-body"><span class="help-block">The program is currently displayed in <strong>(GMT-04:00) Eastern Time (US & Canada)</strong>.</span><div class="row"><div class="col-sm-11 col-sm-offset-1"><label class="radio"><input type="radio" checked="checked" name="9659afaa126198132be460b106e35ccb" value="false" onchange="if( ($(this).val() == 'true' && this.checked) != $('#cec04de0447905c49fb377c6d9693505').is(':visible') ) { $('#cec04de0447905c49fb377c6d9693505').fadeToggle( 250 ); }"/><strong>Use conference time zone: (GMT-04:00) Eastern Time (US & Canada)</strong></label><label class="radio"><input type="radio" name="9659afaa126198132be460b106e35ccb" value="true" onchange="if( ($(this).val() == 'true' && this.checked) != $('#cec04de0447905c49fb377c6d9693505').is(':visible') ) { $('#cec04de0447905c49fb377c6d9693505').fadeToggle( 250 ); }"/>Select other time zone</label><div id="cec04de0447905c49fb377c6d9693505" style=" display: none;"><select name="0e35d6393a8ba494aa0723dd51b6899c" class="select form-control"><option value="" selected="selected" data-utc-minute-offset="0"></option><option value="Etc/GMT+12" data-utc-minute-offset="-720">(GMT-12:00) AoE (Anywhere On Earth)</option><option value="Pacific/Midway" data-utc-minute-offset="-660">(GMT-11:00) Midway Island, Samoa</option><option value="America/Adak" data-utc-minute-offset="-600">(GMT-09:00) Hawaii-Aleutian</option><option value="Etc/GMT+10" data-utc-minute-offset="-600">(GMT-10:00) Hawaii</option><option value="Pacific/Marquesas" data-utc-minute-offset="-570">(GMT-09:30) Marquesas Islands</option><option value="Pacific/Gambier" data-utc-minute-offset="-540">(GMT-09:00) Gambier Islands</option><option value="America/Anchorage" data-utc-minute-offset="-540">(GMT-08:00) Alaska</option><option value="America/Ensenada" data-utc-minute-offset="-480">(GMT-07:00) Tijuana, Baja California</option><option value="Etc/GMT+8" data-utc-minute-offset="-480">(GMT-08:00) Pitcairn Islands</option><option value="America/Los_Angeles" data-utc-minute-offset="-480">(GMT-07:00) Pacific Time (US & Canada)</option><option value="America/Denver" data-utc-minute-offset="-420">(GMT-06:00) Mountain Time (US & Canada)</option><option value="America/Chihuahua" data-utc-minute-offset="-360">(GMT-06:00) Chihuahua, La Paz, Mazatlan</option><option value="America/Dawson_Creek" data-utc-minute-offset="-420">(GMT-07:00) Arizona</option><option value="America/Belize" data-utc-minute-offset="-360">(GMT-06:00) Saskatchewan, Central America</option><option value="America/Cancun" data-utc-minute-offset="-300">(GMT-05:00) Guadalajara, Mexico City, Monterrey</option><option value="Chile/EasterIsland" data-utc-minute-offset="-300">(GMT-05:00) Easter Island</option><option value="America/Chicago" data-utc-minute-offset="-360">(GMT-05:00) Central Time (US & Canada)</option><option value="America/New_York" data-utc-minute-offset="-300">(GMT-04:00) Eastern Time (US & Canada)</option><option value="America/Havana" data-utc-minute-offset="-300">(GMT-04:00) Cuba</option><option value="America/Bogota" data-utc-minute-offset="-300">(GMT-05:00) Bogota, Lima, Quito, Rio Branco</option><option value="America/Caracas" data-utc-minute-offset="-240">(GMT-04:00) Caracas</option><option value="America/Santiago" data-utc-minute-offset="-180">(GMT-03:00) Santiago</option><option value="America/La_Paz" data-utc-minute-offset="-240">(GMT-04:00) La Paz</option><option value="Atlantic/Stanley" data-utc-minute-offset="-180">(GMT-03:00) Faukland Islands</option><option value="America/Campo_Grande" data-utc-minute-offset="-240">(GMT-04:00) Manaus, Amazonas, Brazil</option><option value="America/Goose_Bay" data-utc-minute-offset="-240">(GMT-03:00) Atlantic Time (Goose Bay)</option><option value="America/Glace_Bay" data-utc-minute-offset="-240">(GMT-03:00) Atlantic Time (Canada)</option><option value="America/St_Johns" data-utc-minute-offset="-210">(GMT-02:30) Newfoundland</option><option value="America/Araguaina" data-utc-minute-offset="-180">(GMT-03:00) UTC-3</option><option value="America/Montevideo" data-utc-minute-offset="-180">(GMT-03:00) Montevideo</option><option value="America/Miquelon" data-utc-minute-offset="-180">(GMT-02:00) Miquelon, St. Pierre</option><option value="America/Godthab" data-utc-minute-offset="-180">(GMT-02:00) Greenland</option><option value="America/Argentina/Buenos_Aires" data-utc-minute-offset="-180">(GMT-03:00) Buenos Aires</option><option value="America/Sao_Paulo" data-utc-minute-offset="-180">(GMT-03:00) Brasilia, Distrito Federal, Brazil</option><option value="America/Noronha" data-utc-minute-offset="-120">(GMT-02:00) Mid-Atlantic</option><option value="Atlantic/Cape_Verde" data-utc-minute-offset="-60">(GMT-01:00) Cape Verde Is.</option><option value="Atlantic/Azores" data-utc-minute-offset="-60">(GMT) Azores</option><option value="Etc/UTC" data-utc-minute-offset="0">(UTC) Coordinated Universal Time</option><option value="Europe/Belfast" data-utc-minute-offset="0">(GMT+01:00) Belfast</option><option value="Europe/Dublin" data-utc-minute-offset="0">(GMT+01:00) Dublin</option><option value="Europe/Lisbon" data-utc-minute-offset="0">(GMT+01:00) Lisbon</option><option value="Europe/London" data-utc-minute-offset="0">(GMT+01:00) London</option><option value="Africa/Abidjan" data-utc-minute-offset="0">(GMT) Monrovia, Reykjavik</option><option value="Europe/Amsterdam" data-utc-minute-offset="60">(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna</option><option value="Europe/Belgrade" data-utc-minute-offset="60">(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague</option><option value="Europe/Brussels" data-utc-minute-offset="60">(GMT+02:00) Brussels, Copenhagen, Madrid, Paris</option><option value="Africa/Algiers" data-utc-minute-offset="60">(GMT+01:00) West Central Africa</option><option value="Africa/Windhoek" data-utc-minute-offset="120">(GMT+02:00) Windhoek</option><option value="Europe/Athens" data-utc-minute-offset="120">(GMT+03:00) Athens</option><option value="Asia/Beirut" data-utc-minute-offset="120">(GMT+03:00) Beirut</option><option value="Africa/Cairo" data-utc-minute-offset="120">(GMT+02:00) Cairo</option><option value="Asia/Gaza" data-utc-minute-offset="120">(GMT+03:00) Gaza</option><option value="Africa/Blantyre" data-utc-minute-offset="120">(GMT+02:00) Harare, Pretoria</option><option value="Asia/Jerusalem" data-utc-minute-offset="120">(GMT+03:00) Jerusalem</option><option value="Europe/Minsk" data-utc-minute-offset="180">(GMT+03:00) Minsk</option><option value="Asia/Damascus" data-utc-minute-offset="180">(GMT+03:00) Syria</option><option value="Europe/Moscow" data-utc-minute-offset="180">(GMT+03:00) Moscow, St. Petersburg, Volgograd</option><option value="Africa/Addis_Ababa" data-utc-minute-offset="180">(GMT+03:00) Nairobi</option><option value="Asia/Tehran" data-utc-minute-offset="210">(GMT+03:30) Tehran</option><option value="Asia/Dubai" data-utc-minute-offset="240">(GMT+04:00) Abu Dhabi, Muscat</option><option value="Asia/Yerevan" data-utc-minute-offset="240">(GMT+04:00) Yerevan</option><option value="Asia/Kabul" data-utc-minute-offset="270">(GMT+04:30) Kabul</option><option value="Asia/Yekaterinburg" data-utc-minute-offset="300">(GMT+05:00) Ekaterinburg</option><option value="Asia/Tashkent" data-utc-minute-offset="300">(GMT+05:00) Tashkent</option><option value="Asia/Kolkata" data-utc-minute-offset="330">(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi</option><option value="Asia/Katmandu" data-utc-minute-offset="345">(GMT+05:45) Kathmandu</option><option value="Asia/Dhaka" data-utc-minute-offset="360">(GMT+06:00) Astana, Dhaka</option><option value="Asia/Novosibirsk" data-utc-minute-offset="420">(GMT+07:00) Novosibirsk</option><option value="Asia/Rangoon" data-utc-minute-offset="390">(GMT+06:30) Yangon (Rangoon)</option><option value="Asia/Bangkok" data-utc-minute-offset="420">(GMT+07:00) Bangkok, Hanoi, Jakarta</option><option value="Asia/Krasnoyarsk" data-utc-minute-offset="420">(GMT+07:00) Krasnoyarsk</option><option value="Asia/Hong_Kong" data-utc-minute-offset="480">(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi</option><option value="Asia/Irkutsk" data-utc-minute-offset="480">(GMT+08:00) Irkutsk, Ulaan Bataar</option><option value="Australia/Perth" data-utc-minute-offset="480">(GMT+08:00) Perth</option><option value="Australia/Eucla" data-utc-minute-offset="525">(GMT+08:45) Eucla</option><option value="Asia/Tokyo" data-utc-minute-offset="540">(GMT+09:00) Osaka, Sapporo, Tokyo</option><option value="Asia/Seoul" data-utc-minute-offset="540">(GMT+09:00) Seoul</option><option value="Asia/Yakutsk" data-utc-minute-offset="540">(GMT+09:00) Yakutsk</option><option value="Australia/Adelaide" data-utc-minute-offset="630">(GMT+10:30) Adelaide</option><option value="Australia/Darwin" data-utc-minute-offset="570">(GMT+09:30) Darwin</option><option value="Australia/Brisbane" data-utc-minute-offset="600">(GMT+10:00) Brisbane</option><option value="Australia/Hobart" data-utc-minute-offset="660">(GMT+11:00) Hobart</option><option value="Asia/Vladivostok" data-utc-minute-offset="600">(GMT+10:00) Vladivostok</option><option value="Australia/Lord_Howe" data-utc-minute-offset="660">(GMT+11:00) Lord Howe Island</option><option value="Etc/GMT-11" data-utc-minute-offset="660">(GMT+11:00) Solomon Is., New Caledonia</option><option value="Asia/Magadan" data-utc-minute-offset="660">(GMT+11:00) Magadan</option><option value="Pacific/Norfolk" data-utc-minute-offset="720">(GMT+12:00) Norfolk Island</option><option value="Asia/Anadyr" data-utc-minute-offset="720">(GMT+12:00) Anadyr, Kamchatka</option><option value="Pacific/Auckland" data-utc-minute-offset="780">(GMT+13:00) Auckland, Wellington</option><option value="Etc/GMT-12" data-utc-minute-offset="720">(GMT+12:00) Fiji, Kamchatka, Marshall Is.</option><option value="Pacific/Chatham" data-utc-minute-offset="825">(GMT+13:45) Chatham Islands</option><option value="Pacific/Tongatapu" data-utc-minute-offset="780">(GMT+13:00) Nuku'alofa</option><option value="Pacific/Kiritimati" data-utc-minute-offset="840">(GMT+14:00) Kiritimati</option></select><script type="text/javascript">var tzOffsetMin = new Date().getTimezoneOffset()*-1; var sel = document.getElementsByName('0e35d6393a8ba494aa0723dd51b6899c')[0] var opts = sel.options; for (var opt, j = 0; opt = opts[j]; j++) { if (opt.getAttribute('data-utc-minute-offset') == tzOffsetMin) { sel.selectedIndex = j; break; } } </script></div></div></div><br><span class="help-block"><small><span class="glyphicon glyphicon-info-sign"></span> The GMT offsets shown reflect the offsets <strong>at the moment of the conference</strong>.</small></span></div></div><div class="panel panel-default timeband-panel"><div class="panel-heading clearfix"><div class="panel-title">Time Band</div></div><div class="panel-body"><span class="help-block">By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).<br>The time band will also limit the events that are included in the personal iCalendar subscription service.</span><div class="row"><div class="col-sm-11 col-sm-offset-1"><label class="radio"><input type="radio" checked="checked" name="f1869fcfb40f29e9c9c46042f4fbda2c" value="false" onchange="if( ($(this).val() == 'true' && this.checked) != $('#c2371058bcb9b31dd10e115e7f712708').is(':visible') ) { $('#c2371058bcb9b31dd10e115e7f712708').fadeToggle( 250 ); }"/><strong>Display full program</strong></label><label class="radio"><input type="radio" name="f1869fcfb40f29e9c9c46042f4fbda2c" value="true" onchange="if( ($(this).val() == 'true' && this.checked) != $('#c2371058bcb9b31dd10e115e7f712708').is(':visible') ) { $('#c2371058bcb9b31dd10e115e7f712708').fadeToggle( 250 ); }"/>Specify a time band</label><div id="c2371058bcb9b31dd10e115e7f712708" style=" display: none;"><span class="input-group"><input name="a4e58ac1cd9cfb26fb62ecc29e600148" type="text" value="07:00" class="flatpickr inputDate form-control"/><script type="text/javascript">$("input:not(.flatpickr-input)[name=a4e58ac1cd9cfb26fb62ecc29e600148]").flatpickr({onOpen: function(dateObj, dateStr, instance){ if(dateStr == ''){ instance.jumpToDate( new Date() ); } }, allowInput: true, dateformat: 'H:i', altFormat: 'H:i' , altInput: true, time_24hr: true, noCalendar: true, enableTime : true}); </script><span class="input-group-addon"> - </span><input name="01ff55ee23f3ce1eb7d922f922eb09b1" type="text" value="19:00" class="flatpickr inputDate form-control"/><script type="text/javascript">$("input:not(.flatpickr-input)[name=01ff55ee23f3ce1eb7d922f922eb09b1]").flatpickr({onOpen: function(dateObj, dateStr, instance){ if(dateStr == ''){ instance.jumpToDate( new Date() ); } }, allowInput: true, dateformat: 'H:i', altFormat: 'H:i' , altInput: true, time_24hr: true, noCalendar: true, enableTime : true}); </script></span></div></div></div></div></div><div class="row form-group"><div class="col-sm-offset-2 col-sm-10"><button style="position: absolute; left: -9999px; width: 1px; height: 1px;" onclick='javascript:serverInvoke("https://conf.researchr.org/userProgramSettingsModalConferenceEdition","userProgramSettingsModalConferenceEdition_apply18ec3dfeeecb5c44c1e40a40983898869", [{"name":"context", "value":"ase-2022"},],"form11390898770538530f0e2bbdb67872b491120c5c8a7", this.nextSibling, true,"program-settings-modal"); return false;'></button><a submitid="userProgramSettingsModalConferenceEdition_apply18ec3dfeeecb5c44c1e40a40983898869" href="javascript:void(0)" onclick="javascript:loadImageElem=this;$(this.previousSibling).click()" class="btn btn-primary btn btn-default">Save</a></div></div></form></div><div class="modal-footer"><a href="#" data-dismiss="modal" class="btn btn-default"><span class="glyphicon glyphicon-remove"></span> Close</a></div></div></div></div></div><div class="program-container"><div class="time-zone-warning text-muted hide-in-print"><div class="alert alert-dismissible alert-info"><button type="button" data-dismiss="alert" aria-label="Close" class="close"><span aria-hidden="true">×</span></button><span class="glyphicon glyphicon-info-sign"></span> You're viewing the program in a time zone which is different from your device's time zone <small class="control-time-zone"><a data-toggle="modal" href="#userProgramSettings">change time zone</a></small></div></div><div class="tz-floating-link"><small class="control-time-zone"><a data-toggle="modal" href="#userProgramSettings" title="Change Program Display Configuration" class="btn btn-xs btn-info"><span class="glyphicon glyphicon-wrench"></span> <span class="glyphicon glyphicon-time"></span></a></small></div><script type="text/javascript">var tzOffsetMin = new Date().getTimezoneOffset()*-1; if(tzOffsetMin != -300){ $('.time-zone-warning').toggleClass('visible'); window.displayUserProgamSettingsOnce = true; } </script><div class="hidable day-wrapper"><h4 class="day-header sticky-top"><div><div>Fri 14 Oct</div><p></p><div class="time-zone-info"><small class="text-muted">Displayed time zone: <strong>Eastern Time (US & Canada)</strong> <small class="control-time-zone"><a data-toggle="modal" href="#userProgramSettings">change</a></small></small></div></div></h4><div class="hidable band hour-8"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom C East" data-facet-plenary="Hide plenary sessions" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c13"></td><td><div class="slot-label">08:30 - 10:00</div></td><td colspan="2"><div class="session-info-in-table">Session 1<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" target="_blank" class="text-muted navigate">[Workshop] HILT' 22</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-c-east" target="_blank" class="room-link navigate">Ballroom C East</a><br/><ul> <li>830-840 Opening, S. Tucker Taft and Jerome Hugues</li> </ul> <hr> <ul> <li>840-940 Keynote#1 : Rustan Leino, Senior Principal Engineer, Amazon Web Services <p><strong>Title</strong> Recent experience with developing formally verified software</p> <p><strong>Abstract:</strong> Numerous impressive projects have developed formally verified software. Typically, the participants in such projects have been formal-methods experts. Can verification tools also be used by common software engineers? I will reflect on this question in the context of the most recent AWS Encryption SDK, a verified library developed in a team with no particular background in verification. I will also give an overview of the verification-aware programming language Dafny, which was used in this development.</p> <p><strong>Bio:</strong> K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Throughout his career, he has developed and applied tools for the formal verification of software. The most recent of these is the Dafny language and verifier, which has been used in projects and education for more than a decade. Leino is an ACM Fellow and a recipient of the CAV Award.</p> </li> </ul> <hr> <ul> <li>940-1010 Session #1: Formal methods and applications (part 1) <ol> <li>Daniel Larraz (The University of Iowa) and Cesare Tinelli (The University of Iowa). <p><strong>Title:</strong> Finding Locally Smallest Cut Sets using Max-SMT.</p> <p><strong>Abstract:</strong> Model-based development (MBD) is increasingly being used for system-level development of safety-critical systems. This approach allows safety engineers to leverage the resultant system model created in the MBD process to assess the system’s resilience to component failure. In particular, one fundamental activity is the identification of minimal cut sets (MCSs), i.e, minimal sets of faults that lead to the violation of a safety requirement. Although the construction of a formal system model enables safety engineers to automate the generation process of MCSs, this is usually a computationally expensive task for complex systems. In this paper, we present a method that leverages Max-SMT solvers to efficiently obtain a small set of faults based on a local optimization of the cut set cardinality. Initial experimental results show the effectiveness of the method in generating cut sets that are close or equal to globally optimal solutions (smallest cut sets) while providing an answer 5.6 times faster on average than the standard method to find a smallest cut set.</p> </li> </ol> </li> </ul> </div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="73293aac-2e2d-493f-ab65-815ff5b9ae3a" class="hidable"><td class="track-color c13"></td><td class=" text-right"><div class="text-muted"><div class="start-time">08:30</div><strong>90m</strong></div><div class="event-type">Other</div><span data-facet-track="ASE [Workshop] HILT' 22"></span></td><td><span data-event-star="5457c1bf-4d44-4a26-9c88-41e9eacb24a3" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="5457c1bf-4d44-4a26-9c88-41e9eacb24a3">TBA</a></strong><div class="prog-track">[Workshop] HILT' 22</div><br></td></tr></table></div><div class="hidable band hour-10"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom B" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c22"></td><td><div class="slot-label">10:00 - 10:30</div></td><td colspan="2"><div class="session-info-in-table">Coffee Break<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-social" target="_blank" class="text-muted navigate">Social</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-b" target="_blank" class="room-link navigate">Ballroom B</a><br/></div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="55a1b8d7-0866-42c6-a86f-5819af1de65c" class="hidable"><td class="track-color c22"></td><td class=" text-right"><div class="text-muted"><div class="start-time">10:00</div><strong>30m</strong></div><div class="event-type">Coffee break</div><span data-facet-track="ASE Social"></span></td><td><span data-event-star="21128066-3af9-4f4e-8de2-2215ddaf3637" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="21128066-3af9-4f4e-8de2-2215ddaf3637">Coffee Break</a></strong><div class="prog-track">Social</div><br></td></tr></table></div><div class="hidable band hour-10"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom C East" data-facet-plenary="Hide plenary sessions" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c13"></td><td><div class="slot-label">10:30 - 12:00</div></td><td colspan="2"><div class="session-info-in-table">Session 2<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" target="_blank" class="text-muted navigate">[Workshop] HILT' 22</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-c-east" target="_blank" class="room-link navigate">Ballroom C East</a><br/><ul> <li>1030-1130 Session #1: Formal methods and applications (part 2) <ol> <li> <p>Daniel Larraz (The University of Iowa), Arjun Viswanathan (The University of Iowa), Mickaël Laurent (Université de Paris) and Cesare Tinelli (The University of Iowa).</p> <p><strong>Title:</strong> Beyond model checking of idealized Lustre in Kind 2.</p> <p><strong>Abstract:</strong> This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now provide traceability information between specification and design elements, which can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. Finally, Kind 2 is also able to check whether a component contract is realizable or not, and provide a deadlocking computation and a set of conflicting guarantees when the contract is unrealizable.</p> </li> <li> <p>Danielle Stewart (University of Minnesota) and John Hatcliff (Kansas State University).</p> <p><strong>Title:</strong> An AADL Contract Language Supporting Integrated Model- and Code-Level Verification.</p> <p><strong>Abstract</strong> Model-based systems engineering approaches support the early adoption of a model – a collection of abstractions – of the system under development. The system model can be augmented with key properties of the system including formal specifications of system behavior that codify portions of system and unit-level requirements. There are obvious gaps between the model with formally specified behavior and the deployed system. Previous work on component contract languages has shown how behavior can be specified in models defined using the Architecture Analysis and Design Language (AADL) – a SAE International standard (AS5506C). That work demonstrated the effectiveness of model-level formal methods specification and verification but did not provide a strong and direct connection to system implementations developed using conventional programming languages. In particular, there was no refinement of model-level contracts to programming language-level contracts nor a framework for formally verifying that program code conforms to model-level behavioral specifications. To address these gaps and to enable the practical application of model-contract languages for verification of deployed high-integrity systems, this paper describes the design of GUMBO AADL contract language that integrates and extends key concepts from earlier contract languages. The GUMBO contract language (GCL) is closely aligned to a formal semantics of the AADL run-time framework, which provides a platform- and language-independent specification of AADL semantics. We have enhanced the HAMR AADL code generation framework to translate model-level contracts to programming language-level contracts in the Slang high-integrity language. We demonstrate how the Logika verification tool can automatically verify that Slang-based AADL component implementations conform to contracts, both at the code-level and model-level. Slang-based implementations of AADL systems can be executed directly or compiled to C for deployments on Linux or the seL4 verified microkernel.</p> </li> </ol> </li> </ul> <hr> <ul> <li>1130-1230 Keynote #2: Niko Matsakis, Senior Principal Engineer, Amazon Web Services <p><strong>Title:</strong> a-mir-formality: a formal model for the Rust language</p> <p><strong>Bio:</strong> Nicholas Matsakis is a Senior Principal Engineer at AWS and co-lead of the open source Rust language design team. He has worked on Rust since 2011, and led the design of its “secret sauce”, the borrow checker. He has played a number of other roles in Rust over the years, such as being a member of the Rust core team, the lead of the Rust compiler team, and helping to launch the Rust Foundation. Prior to working on Rust, he completed a PhD at ETH Zurich and did his undergraduate study at MIT.</p> </li> </ul> </div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="82028bf7-cb47-4f38-85e5-80828054c2fb" class="hidable"><td class="track-color c13"></td><td class=" text-right"><div class="text-muted"><div class="start-time">10:30</div><strong>90m</strong></div><div class="event-type">Other</div><span data-facet-track="ASE [Workshop] HILT' 22"></span></td><td><span data-event-star="5457c1bf-4d44-4a26-9c88-41e9eacb24a3" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="5457c1bf-4d44-4a26-9c88-41e9eacb24a3">TBA</a></strong><div class="prog-track">[Workshop] HILT' 22</div><br></td></tr></table></div><div class="hidable band hour-12"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom B" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c22"></td><td><div class="slot-label">12:00 - 13:30</div></td><td colspan="2"><div class="session-info-in-table">Lunch<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-social" target="_blank" class="text-muted navigate">Social</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-b" target="_blank" class="room-link navigate">Ballroom B</a><br/></div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="e2c7e7ea-ce41-4b8c-b017-8227b44dd6f8" class="hidable"><td class="track-color c22"></td><td class=" text-right"><div class="text-muted"><div class="start-time">12:00</div><strong>90m</strong></div><div class="event-type">Lunch</div><span data-facet-track="ASE Social"></span></td><td><span data-event-star="52edb43e-8548-498c-96ca-b8d58a806596" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="52edb43e-8548-498c-96ca-b8d58a806596">Lunch</a></strong><div class="prog-track">Social</div><br></td></tr></table></div><div class="hidable band hour-13"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom C East" data-facet-plenary="Hide plenary sessions" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c13"></td><td><div class="slot-label">13:30 - 15:00</div></td><td colspan="2"><div class="session-info-in-table">Session 3<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" target="_blank" class="text-muted navigate">[Workshop] HILT' 22</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-c-east" target="_blank" class="room-link navigate">Ballroom C East</a><br/><ul> <li>1330-1530 Session #2 : Language and Assurance <ol> <li> <p>David Hardin (Collins Aerospace).</p> <p><strong>Title:</strong> Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero Trust Architecture Development.</p> <p><strong>Abstract:</strong> Zero Trust Architecture requirements are of increasing importance in critical systems development. Zero trust tenets hold that no implicit trust be granted to assets based on their physical or network location. Zero Trust development focuses on authentication, authorization, and shrinking implicit trust zones to the most granular level possible, while maintaining availability and minimizing authentication latency. Performant, high-assurance cryptographic primitives are thus central to successfully realizing a Zero Trust Architecture. The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Our interest in Rust particularly stems from its potential as a hardware/software co-assurance language for developing Zero Trust Architectures. We describe a novel environment enabling Rust to be used as a High-Level Synthesis (HLS) language, suitable for secure and performant Zero Trust application development. Many incumbent HLS languages are a subset of C, and inherit many of the well-known security shortcomings of that language. A Rust-based HLS brings a single modern, type-safe, memory-safe, high-assurance development language for both hardware and software. To study the benefits of this approach, we crafted a Rust HLS subset, and developed a frontend to the hardware/software co-assurance toolchain due to Russinoff and colleagues at Arm, used primarily for floating-point hardware formal verification. This allows us to leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe our Rust subset, detail our prototype toolchain, and describe the implementation, performance analysis, formal verification and validation of representative Zero Trust algorithms and data structures written in Rust, emphasizing cryptographic primitives and common data structures.</p> </li> <li> <p>Claire Dross (AdaCore).</p> <p><strong>Title:</strong> Containers for Specification in SPARK.</p> <p><strong>Abstract:</strong> The SPARK tool performs static analysis of Ada programs. It can be used to verify both that a program is free from runtime exceptions and that it conforms to a specification expressed through contracts. To facilitate dynamic analysis, Ada contracts are regular expressions which can be evaluated at execution. As a result, the annotation language of the SPARK tool is restricted to executable constructs. In this context, high-level concepts necessary for specification by contracts need to be supplied as libraries. For example, the latest version of the Ada language introduces unbounded integers and rational numbers to the standard library. In this article, we present the functional containers library which provides collections suitable for use in specification. We explain how they can be used to specify and verify complex programs through concrete examples that have been developed over many years.</p> </li> <li> <p>S. Tucker Taft (AdaCore).</p> <p><strong>Title:</strong> Rigorous Pattern Matching as a Language Feature.</p> <p><strong>Abstract:</strong> Structural pattern-matching as a language feature has become more common in programming languages over the past decade. This paper will consider more generally the challenge of adding pattern matching as a programming language feature, from the points of view of language design, rigorous static error detection, and effectiveness. In this context, a pattern matching language feature can be seen as providing a more rigorous approach to handling the complex conditionals that arise in processing highly structured input</p> </li> </ol> </li> </ul> </div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="5bc5b004-977e-45a6-96e5-e4209bd56438" class="hidable"><td class="track-color c13"></td><td class=" text-right"><div class="text-muted"><div class="start-time">13:30</div><strong>90m</strong></div><div class="event-type">Other</div><span data-facet-track="ASE [Workshop] HILT' 22"></span></td><td><span data-event-star="5457c1bf-4d44-4a26-9c88-41e9eacb24a3" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="5457c1bf-4d44-4a26-9c88-41e9eacb24a3">TBA</a></strong><div class="prog-track">[Workshop] HILT' 22</div><br></td></tr></table></div><div class="hidable band hour-15"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom B" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c22"></td><td><div class="slot-label">15:00 - 15:30</div></td><td colspan="2"><div class="session-info-in-table">Coffee Break<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-social" target="_blank" class="text-muted navigate">Social</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-b" target="_blank" class="room-link navigate">Ballroom B</a><br/></div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="c1cfe81b-6c6b-4943-9320-c1d8690b73b1" class="hidable"><td class="track-color c22"></td><td class=" text-right"><div class="text-muted"><div class="start-time">15:00</div><strong>30m</strong></div><div class="event-type">Coffee break</div><span data-facet-track="ASE Social"></span></td><td><span data-event-star="21128066-3af9-4f4e-8de2-2215ddaf3637" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="21128066-3af9-4f4e-8de2-2215ddaf3637">Coffee Break</a></strong><div class="prog-track">Social</div><br></td></tr></table></div><div class="hidable band hour-15"><table data-facet-date="Fri 14 Oct 2022" data-facet-date-order="221014" data-facet-room="Ballroom C East" data-facet-plenary="Hide plenary sessions" class="table table-condensed session-table"><colgroup width="10px"/><colgroup width="100px"/><colgroup width="10px"/><colgroup width="100%"/><tr class="session-details"><td class="track-color c13"></td><td><div class="slot-label">15:30 - 17:00</div></td><td colspan="2"><div class="session-info-in-table">Session 4<span class="pull-right"><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" target="_blank" class="text-muted navigate">[Workshop] HILT' 22</a></span> at <a href="https://conf.researchr.org/room/ase-2022/ase-2022-venue-ballroom-c-east" target="_blank" class="room-link navigate">Ballroom C East</a><br/><ul> <li>1530-1700 Session #3 : Use Cases <ol> <li> <p>Tabea Bordis (Karlsruhe Institute of Technology), Tobias Runge (Karlsruhe Institute of Technology), Alexander Kittelmann (Karlsruhe Institute of Technology) and Ina Schaefer (Karlsruhe Institute of Technology).</p> <p><strong>Title:</strong> Correctness-by-Construction: An Overview of the CorC Ecosystem (Short Abstract).</p> <p><strong>Abstract:</strong> Correctness-by-Construction (CbC) is an incremental software development technique in the field of formal methods to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification takes part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules that define side conditions preserving the correctness of the program. This specification-first, refinement-based approach as pursued by CbC has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged over 40 years ago, CbC is not widespread and mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software verification. In this short paper, we give an overview on our research regarding CbC in four different lines of research. For all of them, we provide tool support building the CorC ecosystem that even further enables CbC-based development for different fields of application and size of software systems. Furthermore, we give an outlook on future work that extends on our concepts for CbC.</p> </li> <li> <p>Laura Humphrey (Air Force Research Laboratory).</p> <p><strong>Title:</strong> Basic Formal Verification of a Waypoint Manager for Unmanned Air Vehicles in SPARK.</p> <p><strong>Abstract:</strong> As software becomes more complex, it becomes more difficult to verify its correctness. This poses a particular challenge for autonomous systems, since they are software-intensive and also require strong evidence of correctness in order to be allowed operate in real-world environments. One way to help address this problem is through the use of formal methods, i.e. mathematically-based tools for software and hardware verification. In this paper, we perform formal program verification on a service in OpenUxAS, a free and open source software framework for mission-level, multi-vehicle autonomy. More specifically, we apply the SPARK language and verification toolset to a service that sanity-checks and segments long sequences of vehicle waypoints to prove that it is free of runtime errors.</p> </li> <li> <p>Howard Ausden (Leidos).</p> <p><strong>Title:</strong> Getting to 100% availability in a large C++ and Ada program.</p> <p><strong>Abstract:</strong> Fault tolerance is a key requirement for air traffic control systems. A system failure could lead to hundreds of flights being delayed or cancelled. Using experience from earlier systems a set of techniques were built into our system at inception, including hot standby copies of executables and latest state checkpointed in disk files. As the system matured through formal testing and early site experience additional techniques were added to bolster the MTBF. These include exception safety, runaway process protection, and pro-active monitoring of the system to let us find and fix defects, often without the air traffic controllers being aware. Leidos now has a variety of techniques with defense in depth, and for new developments we scale the number of layers to the difficulty and impact of failure and recovery from the failure. Since Fall 2016, the customer has measured the system as 100% available at all operational sites.</p> </li> </ol> </li> </ul> <hr> <p>1700 - 1715 Conclusion</p> </div></td></tr><tr class="firefox-fix"><td></td><td></td><td></td><td></td></tr><tr data-slot-id="7cbd0e06-fa44-489d-b5c4-955c286fb64a" class="hidable"><td class="track-color c13"></td><td class=" text-right"><div class="text-muted"><div class="start-time">15:30</div><strong>90m</strong></div><div class="event-type">Other</div><span data-facet-track="ASE [Workshop] HILT' 22"></span></td><td><span data-event-star="5457c1bf-4d44-4a26-9c88-41e9eacb24a3" title="Add event to your program"><span class="text-disabled glyphicon glyphicon-star-empty"></span></span></td><td><strong><a href="#" data-event-modal="5457c1bf-4d44-4a26-9c88-41e9eacb24a3">TBA</a></strong><div class="prog-track">[Workshop] HILT' 22</div><br></td></tr></table></div></div></div></div></div></div></div><div class="col-sm-0 sidebar"></div></div><div id="messages-placeholder" class="alert alert-warning" style="display:none;"><a data-dismiss="alert" class="close">x</a><em>Thu 28 Nov 15:43</em></div></div><div id="notifications-ph" class="webdsl-placeholder"></div><div id="event-modal-loader" class="webdsl-placeholder"><form name="form_131600131703c411e65b13378d08eb1f6672b5a0259" id="form_131600131703c411e65b13378d08eb1f6672b5a0259" action="https://conf.researchr.org/eventDetailsModalByAjaxConferenceEdition" accept-charset="UTF-8" method="POST" class="hidden"><input type="hidden" name="form_131600131703c411e65b13378d08eb1f6672b5a0259" value="1" /><input type="hidden" name="context" value="ase-2022" /><input name="ae03f7f6f951d515a297b161e922205d" type="text" value="" class="inputString form-control event-id-input"/><button style="position: absolute; left: -9999px; width: 1px; height: 1px;" onclick='javascript:serverInvoke("https://conf.researchr.org/eventDetailsModalByAjaxConferenceEdition","eventDetailsModalByAjaxConferenceEdition_ia0_3c411e65b13378d08eb1f6672b5a0259", [{"name":"context", "value":"ase-2022"},],"form_131600131703c411e65b13378d08eb1f6672b5a0259", this.nextSibling, false,"event-modal-loader"); return false;'></button><a submitid="eventDetailsModalByAjaxConferenceEdition_ia0_3c411e65b13378d08eb1f6672b5a0259" href="javascript:void(0)" onclick="javascript:loadImageElem=this;$(this.previousSibling).click()" id="load-modal-action"></a></form></div><div id="event-star-form" class="webdsl-placeholder"><form name="form_509860938088b48fd14544d4239b498a2cf339e02b" id="form_509860938088b48fd14544d4239b498a2cf339e02b" action="https://conf.researchr.org/eventStarByAjaxConferenceEdition" accept-charset="UTF-8" method="POST" class="hidden"><input type="hidden" name="form_509860938088b48fd14544d4239b498a2cf339e02b" value="1" /><input type="hidden" name="context" value="ase-2022" /><input name="a0b55aa29cf9431a9461b359872014e3" type="text" value="" class="inputString form-control event-id-input"/><button style="position: absolute; left: -9999px; width: 1px; height: 1px;" onclick='javascript:serverInvoke("https://conf.researchr.org/eventStarByAjaxConferenceEdition","eventStarByAjaxConferenceEdition_ia0_88b48fd14544d4239b498a2cf339e02b", [{"name":"context", "value":"ase-2022"},],"form_509860938088b48fd14544d4239b498a2cf339e02b", this.nextSibling, false,"event-star-form"); return false;'></button><a submitid="eventStarByAjaxConferenceEdition_ia0_88b48fd14544d4239b498a2cf339e02b" href="javascript:void(0)" onclick="javascript:loadImageElem=this;$(this.previousSibling).click()" id="star-event-action"></a></form></div><div id="event-modals" class="webdsl-placeholder"></div><script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; addEventModalLoadOnClick(node); addStarredEventOnClick(node); }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script><footer class="footer"><div class="container"><div class="footer-box"><div class="row"><div class="col-sm-3"><h3><a href="https://conf.researchr.org/home/ase-2022" class="navigate"><span class="glyphicon glyphicon-home"></span> ASE 2022</a></h3><div><a href="https://conf.researchr.org/contact/ase-2022" class="navigate"><span class="glyphicon glyphicon-envelope"></span> contact form</a></div><hr/>using <a href="https://conf.researchr.org" class="navigate">conf.researchr.org</a> (<a href="http://yellowgrass.org/roadmap/conf.researchr.org" class="navigate">v1.67.1</a>)<br/><small><a href="https://conf.researchr.org/support/ase-2022" target="_blank" class="navigate"><span class="glyphicon glyphicon-question-sign"></span> Support page</a></small><br/><small></small></div><div class="col-sm-5"><div class="row"><div class="col-sm-6"><h4>Tracks</h4><a href="https://conf.researchr.org/track/ase-2022/ase-2022-artifact-evaluation" class="navigate">Artifact Evaluation</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-doctoral-symposium" class="navigate">Doctoral Symposium</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-industry-showcase" class="navigate">Industry Showcase</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-journal-first-papers" class="navigate">Journal-first Papers</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-late-breaking-results" class="navigate">Late Breaking Results</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-nier-track" class="navigate">NIER Track</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-research-papers" class="navigate">Research Papers</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-student-research-competition" class="navigate">Student Research Competition</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-student-volunteers" class="navigate">Student Volunteers</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-tool-demonstrations" class="navigate">Tool Demonstrations</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-tutorials" class="navigate">Tutorials</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshops" class="navigate">Workshops</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-a-mobile-22" class="navigate">[Workshop] A-Mobile '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-ase4games-22" class="navigate">[Workshop] ASE4Games '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-aust-22" class="navigate">[Workshop] AUST '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-aesir-22" class="navigate">[Workshop] AeSIR '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hcse-cs-22" class="navigate">[Workshop] HCSE&CS '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-hilt-22" class="navigate">[Workshop] HILT' 22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-iwor-22" class="navigate">[Workshop] IWoR '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-jpf-22" class="navigate">[Workshop] JPF '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-workshop-varse-22" class="navigate">[Workshop] VARSE '22</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-diversity-and-inclusion-events" class="navigate">Diversity and Inclusion Events</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-meetings" class="navigate">Meetings</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-plenary" class="navigate">Plenary</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-mip-awards" class="navigate">MIP Awards</a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-posters-" class="navigate">Posters </a><br/><a href="https://conf.researchr.org/track/ase-2022/ase-2022-keynotes" class="navigate">Keynotes</a></div><div class="col-sm-6"></div></div></div><div class="col-sm-2"><h4>Attending</h4><a href="https://conf.researchr.org/venue/ase-2022/ase-2022-venue" class="navigate">Venue: Oakland Center, Michigan, USA</a><br><a href="https://conf.researchr.org/attending/ase-2022/attendee-information" class="navigate">Attendee Information</a><br><a href="https://conf.researchr.org/attending/ase-2022/presenter-information" class="navigate">Presenter Information</a><br><a href="https://conf.researchr.org/attending/ase-2022/covid-19-protocol" class="navigate">COVID-19 Protocol</a><br><a href="https://conf.researchr.org/attending/ase-2022/registration" class="navigate">Registration</a><br><a href="https://conf.researchr.org/attending/ase-2022/accommodation" class="navigate">Accommodation</a><br><a href="https://conf.researchr.org/attending/ase-2022/visa-letters" class="navigate">Visa Letters</a><br><a href="https://conf.researchr.org/attending/ase-2022/travel-support" class="navigate">Travel Support</a><br><a href="https://conf.researchr.org/attending/ase-2022/diversity-and-inclusion" class="navigate">Diversity and Inclusion</a><br><a href="https://conf.researchr.org/attending/ase-2022/code-of-conduct" class="navigate">Code of Conduct</a></div><div class="col-sm-2"><a href="https://conf.researchr.org/signup/ase-2022" class="navigate">Sign Up</a></div></div></div></div></footer></div><script type="text/javascript">(function(){ var post_process_function = function(n){ var node=(n&&n.nodeType === 1)?n:document; var defaultplacement = $(document).scrollLeft() > 100 ? 'auto left' : 'auto top'; $(node).find('[title]').tooltip({placement: function(tt, elem){ var attval = elem.getAttribute('data-placement'); return attval ? attval : defaultplacement; }, container: false, sanitize: false}); $('.tooltip.fade.in, .ui-tooltip-content').remove(); }; var original_post_process_func = ajax_post_process; ajax_post_process = function(){ original_post_process_func.apply(this,arguments); post_process_function.apply(this,arguments); }; $(document).ready( post_process_function ); })(); </script><script type="text/javascript">jQuery(document).ready(function($) { $(".clickable-row").click(function() { var href = $(this).attr("href"); if( window.location.href.indexOf( href ) < 0 ){ if ($(this).hasClass('new-window') ){ window.open( href ); } else { window.document.location = href; } } }); }); </script></body></html>