-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtrust.html
144 lines (117 loc) · 8.91 KB
/
trust.html
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
<link href="css/metro-bootstrap.css" rel="stylesheet">
<!--<link href="css/metro-bootstrap-responsive.css" rel="stylesheet">-->
<link href="css/iconFont.css" rel="stylesheet">
<!-- Load JavaScript Libraries -->
<script src="js/jquery/jquery.min.js"></script>
<script src="js/jquery/jquery.widget.min.js"></script>
<!-- Metro UI CSS JavaScript plugins -->
<script src="js/load-metro.js"></script>
<!-- Local JavaScript -->
<script src="js/docs.js"></script>
<script src="js/github.info.js"></script>
<title>Yongwang ZHAO's Homepage</title>
<style>
.container {
width: 1040px;
}
</style>
</head>
<body class="metro" style="text-align:justify;">
<div class="container">
<div class="margin10 nrm nlm" data-load="header.html"></div>
<div class="main-content clearfix">
<div class="tab-control" data-role="tab-control" style="float:left;width:100%;">
<!--<ul class="tabs">
<li class="active"><a href="index.html"><b>Home</b>
<i class="icon-arrow-right-5"></i> <b>Research </b> </a></li>
</ul>-->
<!--
<div class="panel" id="journal" data-role="panel" style="width:100%;">
<div class="panel-header" style="background:#dddddd;font-size:14pt;">
<span class="fg-darker"> <b>CORIN - Correctness Infrastructure for Software (软件正确性的基础设施)</b></span>
</div>
<div class="panel-content margin10 fg-dark nlp nrp" style="font-size:13pt;margin-top:-5pt;margin-bottom:-5pt">
-->
<div class="tab-control" data-role="tab-control" style="float:left;">
<div class="panel" id="flat" data-role="panel" style="width:100%;">
<div class="panel-header" style="background:#dddddd;font-size:14pt;">
<span class="fg-darker"> <b>TRust<!--<sup>2</sup>--> - Programming Languages and Trusted Compilers (编程语言与可信编译)</b></span>
</div>
<div class="panel-content margin10 fg-dark nlp nrp" style="width:96%;font-size:13pt;margin-left:15pt;margin-right: 25pt; margin-top:0pt;margin-bottom:0pt">
<!--
<div style="float:right; overflow:hidden; width:280px; margin-left:20pt;">
<div>
<nav class="sidebar light">
<ul>
<li class="active"><a href="#" class="bg-lightBlue" style="font-size:13pt;"><i class="icon-home"></i>Navigation</a></li>
<li class="stick bg-green"><a href="#survey" class="bg-hover-steel"><i class="icon-arrow-right-5"></i>Survey</a></li>
<li class="stick bg-yellow"><a href="#zephyr" class="bg-hover-steel"><i class="icon-arrow-right-5"></i>Zephyr RTOS</a></li>
<li class="stick bg-blue"><a href="#skifs" class="bg-hover-steel"><i class="icon-arrow-right-5"></i>Separation Kernels</a></li>
<li class="stick bg-orange"><a href="#arinc653" class="bg-hover-steel"><i class="icon-arrow-right-5"></i>ARINC653 Standard and OSs</a></li>
<li class="stick bg-orange"><a href="#memory" class="bg-hover-steel"><i class="icon-arrow-right-5"></i>Memory Management</a></li>
</ul>
</nav>
</div>
</div> -->
<div>
<p style="font-size:13pt;">
<b>TRust<!--<sup>2</sup>--></b> is a long-term project focusing on programming languages and trusted compilation by developing formal semantics of languages and formal verification of compiling. The final goal of this project is to create a formally verified compiler for various languages.
</p>
<p style="font-size:13pt;">
In this project, we have created a formal programming language (CSimpl) in Isabelle/HOL. CSimpl is a generic and realistic imperative language by extending Simpl and providing a rely-guarantee proof system for compositional reasoning of concurrent programs and a refinement approach for top-down development of concurrent systems. Simpl is composed of the necessary constructs to capture most of the features present in common sequential languages, such as conditional branching, loops, abrupt termination and exceptions, assertions, mutually recursive functions, expressions with side effects, and nondeterminism. Additionally, Simpl can express memory related features like the memory heap, pointers, and pointers to functions. Simpl is able to represent a large subset of C99 code and has been applied to the formal verification of seL4 OS kernel at C code level.
</p>
<p style="font-size:13pt;">
In this project, we have also developed comprehensive formal semantics of LLVM IR language in Isabelle/HOL, and AADL architecture language and its verification approach in Isabelle/HOL. Using our PiCore framework and integrated languages, we have developed the formal semantics of a core subset of BPEL business process language and a verified compilation of BPEL programs to PiCore specification (<b>see <a href="corin.html#picore">PiCore</a> for more details </b>).
</p>
<div class="panel-header" style="background:#eeeeee;font-size:13pt;">
<span class="fg-darker"> <b>Research Topics and Outcomes</b></span>
</div>
<div class="listview-outlook" style="width:98%;">
<div class="list" id="csimpl">
<div class="list-content" style="font-size:13pt;">
<div class="news_data2">
<a href="#" class="fg-cobalt fg-hover-crimson"><i class="icon-arrow-right-5"></i>
<b>CSimpl: An Imperative Programming Language for Concurrent Systems</b>
</a></br>
<span class="panel-content margin10 fg-dark nlp nrp">
<p>
Developing correct concurrent systems is a large challenge. To provide a programming language and further a formal reasoning system for concurrent systems, we developed CSimpl, a generic and realistic imperative language in Isabelle/HOL theorem prover. CSimpl provides a rely-guarantee proof system for compositional reasoning of concurrent programs and a refinement approach for top-down development of concurrent systems in the correct-by-construct manner.
</p>
<p>
It is essential to deal with the interference of the environment between programs in concurrent program verification. This has led to the development of concurrent program reasoning techniques such as rely-guarantee. However, the source code of the programs to be verified often involves language features such as exceptions and procedures which are not supported by the existing mechanizations of those concurrent reasoning techniques. Schirmer et al. have solved a similar problem for sequential programs by developing a verification framework in the Isabelle/HOL theorem prover called Simpl, which provides a rich sequential language that can encode most of the features in real world programming languages. However Simpl only aims to verify sequential programs, and it does not support the specification nor the verification of concurrent programs. CSimpl is an extension of Simpl with concurrency oriented language features and verification techniques. We prove the compositionality of the CSimpl semantics and we provide inference rules for the language constructors to reason about CSimpl programs using rely-guarantee, showing that the inference rules are sound w.r.t. the language semantics.
</p>
<p>
To support compositional top-down verification of concurrent systems using rely-guarantee, we propose CSim2 a compositional rely-guarantee-based framework for complex concurrent systems in the Isabelle/HOL theorem prover. CSim2 uses CSimpl to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim2 provides a simulation based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations.
</p>
</span>
<ul>
<li>David Sanan, <strong>Yongwang Zhao</strong>, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu, "CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs", <em><u>23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, ETAPS)</u></em>, 22-29 April 2017, Uppsala, Sweden, pp. 481-498 (<em><strong>CCF B, Top conf. in formal methods</strong></em>) <a href="papers/TACAS2017.pdf" target="_blank"><strong>[PDF download]</strong></a>
</li>
<li>
David Sanan, <strong>Yongwang Zhao#</strong>, Yang Liu, Shangwei Lin, "CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee", <em>
<u>ACM Transactions on Programming Languages and Systems (TOPLAS) </u></em>, to appear (<em><strong>CCF A, top journal in programming languages</strong></em>)
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<!--
</div>
</div> -->
</div>
</div>
<footer data-load="footer.html">
</footer>
</div>
<script src="js/hitua.js"></script>
</body>
</html>