Travelled to:
1 × Italy
1 × The Netherlands
4 × USA
Collaborated with:
Robby J.Hatcliff P.Chalin X.Deng H.Thiagarajan D.Hardin P.Courtieu M.Aponte T.Crolard Z.Zhang J.Guitton T.Jennings
Talks about:
contract (3) symbol (3) execut (3) spark (3) check (3) use (3) verif (2) bakar (2) base (2) ada (2)
Person: Jason Belt
DBLP: Belt:Jason
Contributed to:
Wrote 6 papers:
- HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using
- Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
- ICSE-2013-HatcliffRCB #execution #framework #symbolic computation #verification
- Explicating symbolic execution (xSymExe): an evidence-based verification framework (JH, R, PC, JB), pp. 222–231.
- HILT-2012-BeltCHR #ada #automation #contract #using #verification
- Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
- SCAM-2012-ThiagarajanHBR #contract #data flow #developer
- Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK (HT, JH, JB, R), pp. 132–137.
- SIGAda-2011-BeltHRCHD #contract #execution #symbolic computation #using
- Enhancing spark’s contract checking facilities using symbolic execution (JB, JH, R, PC, DH, XD), pp. 47–60.
- ESEC-FSE-2009-BeltRD #analysis #lightweight #optimisation #symbolic computation
- Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses (JB, R, XD), pp. 355–364.