NetKAT: Semantic foundations for networks CJ Anderson, N Foster, A Guha, JB Jeannin, D Kozen, C Schlesinger, ... Acm sigplan notices 49 (1), 113-126, 2014 | 512 | 2014 |
A formally verified hybrid system for the next-generation airborne collision avoidance system JB Jeannin, K Ghorbal, Y Kouskoulas, R Gardner, A Schmidt, E Zawadzki, ... Tools and Algorithms for the Construction and Analysis of Systems: 21st …, 2015 | 91 | 2015 |
I4: incremental inference of inductive invariants for verification of distributed protocols H Ma, A Goel, JB Jeannin, M Kapritsos, B Kasikci, KA Sakallah Proceedings of the 27th ACM Symposium on Operating Systems Principles, 370-384, 2019 | 52 | 2019 |
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system JB Jeannin, K Ghorbal, Y Kouskoulas, A Schmidt, R Gardner, S Mitsch, ... International Journal on Software Tools for Technology Transfer 19, 717-741, 2017 | 47 | 2017 |
Formal verification of ACAS X, an industrial airborne collision avoidance system JB Jeannin, K Ghorbal, Y Kouskoulas, R Gardner, A Schmidt, E Zawadzki, ... 2015 International Conference on Embedded Software (EMSOFT), 127-136, 2015 | 42 | 2015 |
Correct by construction networks using stepwise refinement L Ryzhyk, N Bjørner, M Canini, JB Jeannin, C Schlesinger, DB Terry, ... USENIX Association Berkeley, CA, USA, 2017 | 40 | 2017 |
Type inference for static compilation of JavaScript S Chandra, CS Gordon, JB Jeannin, C Schlesinger, M Sridharan, F Tip, ... ACM SIGPLAN Notices 51 (10), 410-429, 2016 | 38 | 2016 |
IOTA: a calculus for internet of things automation JL Newcomb, S Chandra, JB Jeannin, C Schlesinger, M Sridharan Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas …, 2017 | 33 | 2017 |
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems JB Jeannin, A Platzer Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as …, 2014 | 29 | 2014 |
Cocaml: Functional programming with regular coinductive types JB Jeannin, D Kozen, A Silva Fundamenta Informaticae 150 (3-4), 347-377, 2017 | 28 | 2017 |
Hybrid theorem proving of aerospace systems: Applications and challenges K Ghorbal, JB Jeannin, E Zawadzki, A Platzer, GJ Gordon, P Capell Journal of Aerospace Information Systems 11 (10), 702-713, 2014 | 24 | 2014 |
Verifying aircraft collision avoidance neural networks through linear approximations of safe regions KD Julian, S Sharma, JB Jeannin, MJ Kochenderfer arXiv preprint arXiv:1903.00762, 2019 | 22 | 2019 |
Language constructs for non-well-founded computation JB Jeannin, D Kozen, A Silva Programming Languages and Systems: 22nd European Symposium on Programming …, 2013 | 21 | 2013 |
Computing with capsules JB Jeannin, D Kozen Descriptional Complexity of Formal Systems: 14th International Workshop …, 2012 | 21 | 2012 |
dkal ⋆ : Constructing Executable Specifications of Authorization Protocols JB Jeannin, G de Caso, J Chen, Y Gurevich, P Naldurg, N Swamy Engineering Secure Software and Systems: 5th International Symposium, ESSoS …, 2013 | 14 | 2013 |
CoCaml: Programming with coinductive types JB Jeannin, D Kozen, A Silva | 12 | 2012 |
Formal verification of safety buffers for sate-based conflict detection and resolution H Herencia-Zapana, JB Jeannin, CA Munoz 27th International Congress of the Aeronautical Sciences (ICAS 2010), 2010 | 12 | 2010 |
Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics Y Kouskoulas, D Genin, A Schmidt, JB Jeannin Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 10 | 2017 |
A physics-based finite-state abstraction for traffic congestion control H Rastgoftar, JB Jeannin 2021 American Control Conference (ACC), 237-242, 2021 | 9 | 2021 |
Towards automatic inference of inductive invariants H Ma, A Goel, JB Jeannin, M Kapritsos, B Kasikci, KA Sakallah Proceedings of the Workshop on Hot Topics in Operating Systems, 30-36, 2019 | 8 | 2019 |