jm + dynamic   3

bcc
Dynamic tracing tools for Linux, a la dtrace, ktrace, etc. Built using BPF, using kernel features in the 4.x kernel series, requiring at least version 4.1 of the kernel
linux  tracing  bpf  dynamic  ops 
april 2016 by jm
Combining static model checking with dynamic enforcement using the Statecall Policy Language
This looks quite nice -- a model-checker "for regular programmers". Example model for ping(1):

<pre>01 automaton ping (int max_count, int count, bool can_timeout) {
02 Initialize;
03 during {
04 count = 0;
05 do {
06 Transmit_Ping;
07 either {
08 Receive_Ping;
09 } or (can_timeout) {
10 Timeout_Ping;
11 };
12 count = count + 1;
13 } until (count &gt;= max_count);
14 } handle {
15 SIGINFO;
16 Print_Summary;
17 };</pre>
ping  model-checking  models  formal-methods  verification  static  dynamic  coding  debugging  testing  distcomp  papers 
march 2015 by jm

Copy this bookmark:



description:


tags: