-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html.failedexperiment
More file actions
57 lines (50 loc) · 10.2 KB
/
index.html.failedexperiment
File metadata and controls
57 lines (50 loc) · 10.2 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
<html>
<head>
<!--<meta http-equiv="refresh" content="2;url=https://www.aere.iastate.edu/modelchecker/" /> -->
<title>Main page</title>
</head>
<body>
<main role="main" id="main-content" class="">
<div class="container">
<h1 class="entry-title screen-reader-text">Home</h1> <article id="homepage" class="post-7 page type-page status-publish hentry">
<div class="entry-content">
<h1>Abstract</h1>
<p>Safety-critical and security-critical systems are entering our lives at an increasingly rapid pace. These are the systems that help fly our planes, drive our cars, deliver our packages, ensure our electricity, or even automate our homes. Especially when humans cannot perform a task in person, e.g., due to a dangerous working environment, we depend on such systems. Before any safety-critical system launches into the human environment, we need to be sure it is really safe. Model checking is a popular and appealing way to rigorously check for safety: given a system, or an accurate model of the system, and a safety requirement, model checking is a “push button” technique to produce either a proof that the system always operates safely, or a counterexample detailing a system execution that violates the safety requirement. Many aspects of model checking are active research areas, including more efficient ways of reasoning about the system’s behavior space, and faster search algorithms for the proofs and counterexamples.</p>
<p>As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don’t have support for expressive specification languages needed for verifying real systems. Our goal is to fill the current gap in model checking research platforms: building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. We will create a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. To add new modeling languages or algorithms, researchers need only to develop a translator to/from the new intermediate language, and will then be able to integrate each advance with the full state-of-the-art in model checking. This community infrastructure will be ideal for catapulting formal verification efforts in many cutting-edge application areas, including security, networking, and operating system verification. We particularly target outreach to the embedded systems (CPS) community as our new framework will make hardware verification problems from this community more accessible.</p>
<hr/>
<div class='gf_browser_chrome gform_wrapper gpoll_enabled_wrapper gpoll_show_results_link_wrapper gpoll_block_repeat_voters_wrapper gpoll_wrapper gform_legacy_markup_wrapper' id='gform_wrapper_1' >
<div class='gform_heading'>
<h3 class="gform_title">Tool Name Vote</h3>
</div><form method='post' enctype='multipart/form-data' id='gform_1' class='gpoll_enabled gpoll_show_results_link gpoll_block_repeat_voters gpoll gform_legacy_markup' action='/modelchecker/' novalidate>
<div class='gform_body gform-body'><ul id='gform_fields_1' class='gform_fields top_label form_sublabel_below description_below'><li id="field_1_4" class="gfield gfield_contains_required field_sublabel_below field_description_below gfield_visibility_visible gpoll_field" data-field-class="gpoll_field"><label class="gfield_label">Vote for your favorite or suggest another<span class="gfield_required"><span class="gfield_required gfield_required_asterisk">*</span></span></label><div class="ginput_container ginput_container_radio"><ul class="gfield_radio" id="input_1_4"><li class="gchoice gchoice_1_4_5"><input name="input_4" type="radio" value="CMC (as in Community Model Checker, has some symmetry)" id="choice_1_4_5"/><label for="choice_1_4_5" id="label_1_4_5">CMC (as in Community Model Checker, has some symmetry)</label></li><li class="gchoice gchoice_1_4_3"><input name="input_4" type="radio" value="Alliance" id="choice_1_4_3"/><label for="choice_1_4_3" id="label_1_4_3">Alliance</label></li><li class="gchoice gchoice_1_4_4"><input name="input_4" type="radio" value="Collective" id="choice_1_4_4"/><label for="choice_1_4_4" id="label_1_4_4">Collective</label></li><li class="gchoice gchoice_1_4_2"><input name="input_4" type="radio" value="Collaboration" id="choice_1_4_2"/><label for="choice_1_4_2" id="label_1_4_2">Collaboration</label></li><li class="gchoice gchoice_1_4_1"><input name="input_4" type="radio" value="Fusion" id="choice_1_4_1"/><label for="choice_1_4_1" id="label_1_4_1">Fusion</label></li><li class="gchoice gchoice_1_4_6"><input name="input_4" type="radio" value="MagiC(M and C for model checker)" id="choice_1_4_6"/><label for="choice_1_4_6" id="label_1_4_6">MagiC(M and C for model checker)</label></li><li class="gchoice gchoice_1_4_0"><input name="input_4" type="radio" value="Ring (as in coming full circle in connecting all areas of model checking, also the one ring to unite them all)" id="choice_1_4_0"/><label for="choice_1_4_0" id="label_1_4_0">Ring (as in coming full circle in connecting all areas of model checking, also the one ring to unite them all)</label></li><li class="gchoice gchoice_1_4_7"><input name="input_4" type="radio" value="gf_other_choice" id="choice_1_4_7" onfocus="jQuery(this).next('input').focus();"/><input class="small" id="input_1_4_other" name="input_4_other" type="text" value="Other" aria-label="Other" onfocus="jQuery(this).prev("input")[0].click(); if(jQuery(this).val() == "Other") { jQuery(this).val(""); }" onblur="if(jQuery(this).val().replace(" ", "") == "") { jQuery(this).val("Other"); }"/></li></ul></div></li><li id="field_1_5" class="gfield gfield_contains_required field_sublabel_below field_description_below gfield_visibility_visible" ><label class='gfield_label gfield_label_before_complex' >Email<span class="gfield_required"><span class="gfield_required gfield_required_asterisk">*</span></span></label><div class='ginput_complex ginput_container ginput_container_email' id='input_1_5_container'>
<span id='input_1_5_1_container' class='ginput_left'>
<input class='' type='email' name='input_5' id='input_1_5' value='' aria-required="true" aria-invalid="false" />
<label for='input_1_5' >Enter Email</label>
</span>
<span id='input_1_5_2_container' class='ginput_right'>
<input class='' type='email' name='input_5_2' id='input_1_5_2' value='' aria-required="true" aria-invalid="false" />
<label for='input_1_5_2' >Confirm Email</label>
</span>
<div class='gf_clear gf_clear_complex'></div>
</div></li><li id="field_1_9" class="gfield field_sublabel_below field_description_below gfield_visibility_visible" ><label class='gfield_label gfield_label_before_complex' >Would you like to signup for a mailing list using the above email?</label><div class='ginput_container ginput_container_checkbox'><ul class='gfield_checkbox' id='input_1_9'><li class='gchoice gchoice_1_9_1'>
<input class='gfield-choice-input' name='input_9.1' type='checkbox' value='Yes' id='choice_1_9_1' />
<label for='choice_1_9_1' id='label_1_9_1'>Yes</label>
</li></ul></div></li><li id="field_1_6" class="gfield field_sublabel_below field_description_below gfield_visibility_visible" ><label class='gfield_label screen-reader-text' for='input_1_6' ></label><div id='input_1_6' class='ginput_container ginput_recaptcha' data-sitekey='6LcsssoZAAAAAHqkDhsM3eJIS2mhDCb0X3mzdiyb' data-theme='light' data-tabindex='-1' data-size='invisible' data-badge='inline'></div></li><li id="field_1_10" class="gfield gform_validation_container field_sublabel_below field_description_below gfield_visibility_visible" ><label class='gfield_label' for='input_1_10' >Name</label><div class='ginput_container'><input name='input_10' id='input_1_10' type='text' value='' autocomplete='new-password'/></div><div class='gfield_description' id='gfield_description_1_10'>This field is for validation purposes and should be left unchanged.</div></li></ul></div>
<div class='gform_footer top_label'> <input type='submit' id='gform_submit_button_1' class='gform_button button' value='Submit' onclick='if(window["gf_submitting_1"]){return false;} if( !jQuery("#gform_1")[0].checkValidity || jQuery("#gform_1")[0].checkValidity()){window["gf_submitting_1"]=true;} ' onkeypress='if( event.keyCode == 13 ){ if(window["gf_submitting_1"]){return false;} if( !jQuery("#gform_1")[0].checkValidity || jQuery("#gform_1")[0].checkValidity()){window["gf_submitting_1"]=true;} jQuery("#gform_1").trigger("submit",[true]); }' />
<input type='hidden' class='gform_hidden' name='is_submit_1' value='1' />
<input type='hidden' class='gform_hidden' name='gform_submit' value='1' />
<input type='hidden' class='gform_hidden' name='gform_unique_id' value='' />
<input type='hidden' class='gform_hidden' name='state_1' value='WyJbXSIsIjNmZDE4MWZmNzQ5N2ZjNDhjMmUxYWMwNjc5MTc1OTU4Il0=' />
<input type='hidden' class='gform_hidden' name='gform_target_page_number_1' id='gform_target_page_number_1' value='0' />
<input type='hidden' class='gform_hidden' name='gform_source_page_number_1' id='gform_source_page_number_1' value='1' />
<input type='hidden' name='gform_field_values' value='' />
</div>
</form>
</div>
</div><!-- .entry-content -->
</article><!-- #homepage -->
</div>
</main>
<!-- /main -->
</body>
</html>