-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
64 lines (58 loc) · 3.06 KB
/
index.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
<!DOCTYPE html
PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<html>
<head>
<link href="css/openjml.css" rel="STYLESHEET" type="text/css" />
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<title>David R. Cok</title>
<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']], displayMath: [ ['$$','$$'], ["\\[","\\]"] ]
}});
</script>
</head>
<body>
<h1>David R. Cok - Consulting and scientific activities</h1>
Trial C: $ a \ll b $ or \( a \ll b \) or $$ a \ll \pi $$ or \[ a \ll \pi \]
Link: <a href="temp/DafnyRef">Ref</a>
<B>Software safety and security:</B> <BR>
I improve software safety and security <BR>
-- ensuring that software does what it is supposed to (safety) <BR>
and does not allow what it is not supposed to (security) --
<UL>
<LI>by working with clients to review and improve their software, using modern
program analysis tools to reason about and detect errors in software
<LI>and my own research and publication in software specification,
verification, and correctness.
</UL>
<h2>Current Professional Activities</h2>
<UL>
<LI>Consulting to improve or validate software (2017 - present)
<LI>Visiting scientist at
<a href="http://www-list.cea.fr/en/technological-research/research-programmes/embedded-systems/validation-and-verification">the LSL lab at CEA</a> (near Paris, France), contributing to the ACSL++ extension of ACSL to C++ and the frama-clang plugin to Frama-C to support verification of C++ programs with specifications written in ACSL++
<LI>Significant contributor to <a href="http://www.jmlspecs.org">JML</a> (the Java Modeling Language) for writing behavioral specifications for Java
<LI>Principal developer of the open source tool <a href="http://www.openjml.org">OpenJML</a> to verify Java programs against JML specifications.
<LI>Contributor to the <a href="http://frama-c.com/download.html">ACSL</a> specification
language for C programs
<LI>Contributor to <a href="http://smt-lib.org">SMT-LIB</a>, a standard language for interacting with SMT solvers
</UL>
<h2>Scientific community</h2>
<UL>
<LI>Proposal reviews and project evaluations for the European Union's research agenda (2010 - present)
<LI>Program committees - many
<LI>Journal article reviews - many
<LI>Organizer of the SMTCOMP competition among SMT solvers (2012-2014)
</UL>
<h2>Past activities</h2>
<UL>
<LI>VP and senior scientist at <a href="http://grammatech.com">GrammaTech</a> (2010 - 2017)
<LI>Senior research scientist and research manager at Kodak Research Lab (1982 - 2010)
<LI>Postdoc at Argonne National Lab (1980 - 1982)
<LI>Ph.D. (1980) (and Masters - 1977) in Physics from Harverd University
<LI>A.B. degrees in Mathematics and in Physics, Calvin College (1975)
</UL>
</body>
</html>