psubotic.github.io/index.html at master · psubotic/psubotic.github.io · GitHub

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
145
146
147
<!DOCTYPE html>
<html>
  <head>
    <meta charset='utf-8'>
    <meta http-equiv="X-UA-Compatible" content="chrome=1">

    <link rel="stylesheet" type="text/css" href="stylesheets/stylesheet.css" media="screen">
    <link rel="stylesheet" type="text/css" href="stylesheets/github-dark.css" media="screen">
    <link rel="stylesheet" type="text/css" href="stylesheets/print.css" media="print">

    <title>Pavle Subotic</title>
  </head>

  <body>

    <header>
      <div class="container">
        <h1>Pavle Subotic</h1>

        <section id="downloads">
          <a href="https://github.com/psubotic" class="btn btn-github"><span class="icon"></span>View on GitHub</a>
        </section>
      </div>
    </header>

    <div class="container">
      <section id="main_content">
        <p><strong>Pavle Subotic </strong><span style="font-size:0.7em">PhD (UCL)</span></p>

<p>
<h2>
<a id="intro" class="anchor" href="#intro" aria-hidden="true"><span aria-hidden="true" class="octicon octicon-link"></span></a>Intro</h2>

<p>I am interested in researching and engineering solutions to large-scale industrial problems, in particular relating to
  Verifiers, Compilers, Databases, and Distributed Systems.

  I have a PhD from <a href="https://www.ucl.ac.uk/">University College London (UCL)</a>

   <ul>

  <li>   I am leading a team that investigates novel mechanisms to improve <a href=https://www.banklesstimes.com/articles/2025/03/27/sonic-labs-introduce-soniccs-2-0-faster-consensus-reduced-memory/>performance</a> and <a href = https://blog.soniclabs.com/an-inside-look-into-sonic-researchs-formal-model-driven-development-process>security</a> for the Sonic blockchain. </li>

   <li>   I was a Snr. Research Software Engineer at Microsoft. I primarily investigated and developed
     provenance and <a href = "https://github.com/microsoft/NBLyzer">static analysis tools</a> for data science.

     <li>  I was a Snr. Applied Scientist at Amazon where I led the automated contract driven development process at Prime Video by founding and
      leading the development of the
  <a href = https://www.amazon.science/latest-news/how-awss-automated-reasoning-group-helps-make-aws-and-other-amazon-products-more-secure>Coastguard</a> tool
      among many other <a href="https://www.youtube.com/watch?v=FPCZ2TIxrpg&t=8888s">projects</a>. </li>

   <li>  I was a visiting researcher at AWS where I founded and co-developed
  <a href = https://www.csoonline.com/article/3298166/what-are-amazon-zelkova-and-tiros-aws-looks-to-reduce-s3-configuration-errors.html>Tiros</a>,
     a tool that analyses Ec2 networks for security vulnerabilities. </li>

   <li> I spent a year at Oracle Labs where I worked on
      <a href = "https://labs.oracle.com/pls/apex/f?p=LABS:project_details:0:134">Souffle</a> with my collegues Prof. Bernhard Scholz and Herbert Jordan. (See LPOP'22 talk <a href="https://www.youtube.com/watch?v=mHVIdHLp9ZQ">here</a>) </li>

   <li>   I was an R&D software
      engineer @ <a href = https://www.optiver.com>Optiver</a>, <a href = https://www.youtube.com/watch?v=ybWXSRx_Lzk>Toshiba R&D</a> and
      <a href=https://www.csiro.au/>CSIRO</a>. During my undergraduate studies I was a summer scholar at NICTA (now Data61) where I worked on hardware and processor simulation for
    the sel4 microkernal verification project. </li>
      </lu>


<!--
<h2>
<a id="Tools" class="anchor" href="#patents" aria-hidden="true"><span aria-hidden="true" class="octicon octicon-link"></span></a>PhD Interns:</h2>
<ul>
<li> @Microsoft: Filip Drobnjakovic, University of Belgrade (ETF), <br> <small>Topic: Investigating Precision and Scale for Data Leakage Analysis</small>
<li> @Microsoft: Slobodan Jenko, University of Belgrade (PMF), <br> <small>Topic: Scalable Static Analysis of Neural Networks</small>
<li> @Microsoft: Uros Bojanic, University of Belgrade (ETF), <br> <small>Topic: Static Analysis for Data Science</small>
<li> @Microsoft: Lazar Milikic, École Polytechnique, <br> <small>Topic: Code Impact Analysis for Notebooks</small>
<li> @Amazon: Djordje Zikelic, IST Austria, <br> <small>Topic: Differential Bloat Analysis</small>
<li> @Amazon: Thomas Seed, University of Kent <br> <small> Topic: A Scalable Latice-based Datalog Engine</small>
<li> @Amazon: Alen Arslanagic, University of Groningen <br> <small> Topic: Log Leakage Analysis</small>
<li> @Amazon: Toan Ngyuen, National University of Singapore <br> <small>Topic: Succinct Explanations for Static Analysis Results</small>
</ul>
-->


 </section>

  <h2>
<a id="intro" class="anchor" href="#intro" aria-hidden="true"><span aria-hidden="true" class="octicon octicon-link"></span></a>Publications</h2>
<ol>
<li><b>A Fast Ethereum-Compatible Forkless Database, TBD<br><small>Herbert Jordan, Kamil Jezek, Pavle Subotic, Bernhard Scholz</small> <small>(<a href=https://arxiv.org/abs/2512.04735>paper</a>)</small></li>
<li><b>Efficient Forkless Blockchain Databases, IEEE Access<br><small>Herbert Jordan, Kamil Jezek, Pavle Subotic, Bernhard Scholz</small> <small>(<a href=https://arxiv.org/abs/2508.20686>paper</a>)</small></li>
<li><b>Static Analysis by Abstract Interpretation Against Data Leakage in Machine Learning, Science of Computer Programming<br><small>Caterina Urban, Filip Drobnjakovic, Pavle Subotic  </small>  <small>(<a href=./papers/Dataleakage_Journal.pdf>paper</a>)</small></li>
<li><b>Formal Model Guided Conformance Testing for Blockchains, TBD<br><small> Filip Drobnjaković, Amir Kashapov, Matija Kupresanin, Bernhard Scholz, Pavle Subotić </small><small>(<a href=https://arxiv.org/abs/2501.08550>paper</a>)</small></li>
<li><b>Formal Verification of a Fail-Safe Cross-Chain Bridge, FMBC'25<br><small> Filip Marić, Bernhard Scholz, Pavle Subotic </small><small>(<a href=https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.8/OASIcs.FMBC.2025.8.pdf>paper</a>)</small></li>
<li><b>Reusable Formal Verification of DAG-based Consensus Protocols, NFM'25<br><small> Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotić </small><small>(<a href=https://arxiv.org/abs/2407.02167>paper</a>)</small></li>
<li><b>Provenance Guided Rollback Suggestions, Theory and Practice of Logic Programming<br><small>David Zhao, Pavle Subotic, Mukund Raghothaman and Bernhard Scholz </small><small>(<a href=https://arxiv.org/pdf/2501.09225>paper</a>)</small></li>
<li><b>Abstract Interpretation-Based Data Leakage Static Analysis, TASE'24<br><small> Filip Drobnjakovic, Pavle Subotic, Caterina Urban </small>  <small>(<a href=./papers/paper_8.pdf>paper</a>)</small></li>
<li><b>Ambit: Verification of Azure RBAC, CCSW@CCS'23<br><small> Matija Kupresanin and Pavle Subotic</small> <small>(<a href=./papers/CCSW23.pdf>paper</a>)</small></li>
<li><b>Program Repair Guided by Datalog-Defined Static Analysis, ESEC/FSE'23<br><small> Yu Liu, Sergey Mechtaev, Pavle Subotic, and Abhik Roychoudhury</small> <small>(<a href=./papers/fSE23.pdf>paper</a>)</small></li>
<li><b>Bit-Vector Typestate Analysis, Formal Aspects of Computing <br> <small> Alen Arslanagic, Pavle Subotic, Jorge Perez</small> <small>(<a href=https://dl.acm.org/doi/pdf/10.1145/3595299>paper</a>)</small></li>
<li><b>Automatically Resolving Data Source Dependency Hell in Large Scale Data Science Projects, CAIN'23	<br><small> Laurent Boué, Pratap Kunireddy, Pavle Subotic </small><small>(<a href=/papers/CAIN.pdf>paper</a>)</small> <small>(<a href=https://arxiv.org/abs/2212.07951>ext paper</a>)</small></li>
<li><b>Geyser: Provenance Extraction and Applications over Data Science Scripts, SIGMOD'23<br><small> F.Psallidas, M.Leszczynski, M.Namaki, A.Floratou, A.Agrawal, K.Karanasos, S.Krishnan, P.Subotic, M.Weimer, Y.Wu, Y.Zh</small> <small>(<a href=./papers/SIGMOD.pdf>paper</a>)</small></li>
<li><b>Efficient SMT-based Network Fault Tolerance Verification, FM'23<br><small> Yu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev and Abhik Roychoudhury</small> <small>(<a href=./papers/FM23.pdf>paper</a>)</small></li>
<li><b>Automatic Rollback Suggestions for Incremental Datalog Evaluation, PADL'23<br><small> David Zhao, Pavle Subotic, Mukund Raghothaman and Bernhard Scholz</small> <small>(<a href=./papers/PADL.pdf>paper</a>)</small></li>
<li><b>Building a Join Optimizer for Souffle, LOPSTR'22<br><small> Samuel Arch, Xiaowen Hu, David Zhao,Pavle Subotic, Bernhard Scholz</small> <small>(<a href=./papers/lopstr2022.pdf>paper</a>)</small></li>
<li><b>Statically Detecting Data Leakages in Data Science Code, SOAP@PLDI'22 <br> <small> Pavle Subotic, Uros Bojanic, Milan Stojic</small> <small>(<a href=./papers/DL.pdf>paper</a>)</small></li>
<li><b>Scalable Typestate Analysis for Low-Latency Environments</a>, iFM'22 <br> <small> Alen Arslanagic, Pavle Subotic, Jorge Perez</small> <small>(<a href=./papers/iFM.pdf>paper</a>)</small></li>
<li><b>A Static Analysis Framework for Data Science Notebooks, ICSE'22 <br> <small> Pavle Subotic, Lazar Milikic, Milan Stojic</small> <small>(<a href=./papers/ICSE.pdf>paper</a>)</small></li>
<li><b>Towards Elastic Incrementalization for Datalog, PPDP'21 <br> <small> David Zhao, Pavle Subotic, Muhund Raghothaman, Bernhard Scholz </small> <small>(<a href=./papers/PPDP.pdf>paper</a>)</small></li>
<li><b>A Scalable Provenance Evaluation Strategy for Datalog</b>, TOPLAS/POPL'21 <br> <small>David Zhao, Pavle Subotic, Bernhard Scholz </small> <small>(<a href=./papers/toplas20.pdf>paper</a>)</small></li>
<li><b>Specializing Parallel Data Structures for Datalog</b>, CCPE Volume 34 <br> <small>Herbert Jordan, Pavle Subotic, David Zhao, Bernhard Scholz</small> <small>(<a href=https://onlinelibrary.wiley.com/doi/full/10.1002/cpe.5643>paper</a>)</small></li>
<li><b>Fast Parallel Equivalence Relations in a Datalog Compiler</b>, PACT'19 <br> <small>Patrick Nappa, David Zhao, Pavle Subotic, Bernhard Scholz</small> <small>(<a href=./papers/pact2019eqrel.pdf>paper</a>)</small></li>
<li><b>Reachability Analysis for AWS-based Networks</b>, CAV'19 <br> <small>Pavle Subotic, Byron Cook and many other authors </small> <small>(<a href=./papers/CAV19.pdf>paper</a>)</small></li>
<li><b>Brie: A Specialized Trie for Concurrent Datalog</b>, PMAM@PPoPP'19 <br> <small>Herbert Jordan, Pavle Subotic, David Zhao, Bernhard Scholz </small> <small>(<a href=./papers/pmam19.pdf>paper</a>)</small></li>
<li><b>A Specialized B-Tree for Concurrent Datalog Evaluation</b>, PPoPP'19 <br> <small>Herbert Jordan, Pavle Subotic, David Zhao, Bernhard Scholz </small> <small>(<a href=./papers/ppopp19.pdf>paper</a>)</small></li>
<li><b>Automatic Index Selection for Large-Scale Datalog Computation</b>, VLDB'19 <br> <small>Pavle Subotic, Herbert Jordan, Lijun Chang, Alan Fekete, Bernhard Scholz </small> <small>(<a href=./papers/p141-subotic.pdf>paper</a>)</small></li>
<li><b>Two concurrent data structures for efficient datalog query processing</b>, PPOPP'18 <br> <small>Herbert Jordan, Bernhard Scholz, Pavle Subotic</small> <small>(<a href=https://dl.acm.org/doi/10.1145/3178487.3178525>paper</a>)</small></li>
<li><b>Souffle: On Synthesising Program Analyzers</b>, CAV'16 <br> <small>Herbert Jordan, Bernhard Scholz, Pavle Subotic </small> <small>(<a href=./papers/cav16.pdf>paper</a>) </small></li>
<li><b>On fast large-scale program analysis in Datalog</b>, CC'16 <br> <small>Bernhard Scholz, Herbert Jordan, Pavle Subotic, Till Westmann</small> <small>(<a href=./papers/cc16.pdf>paper</a>)</small> </li>
<li><b>Guiding Craig Interpolation with Domain-specific Abstractions</b>, Acta Informatica, Issue 53 <br> <small>Jerome Leurox, Philipp Rümmer, Pavle Subotic</small> <small>(<a href=./papers/acta2015.pdf>paper</a>) </small> </li>
<li><b>Horn Clauses for Communicating Timed Systems</b>, HCVS'14 <br> <small> Hossein Hojjat, Philipp Rümmer, Pavle Subotic, Wang Yi</small> <small>(<a href=./papers/HCVS.pdf>paper</a>)</small></li>
<li><b>Exploring interpolants</b>, FMCAD'13 <br> <small> Philipp Rümmer, Pavle Subotic</small> <small>(<a href=./papers/exploring-interpolants.pdf>paper</a>)</small></li>
<li><b>Logico-Numerical Max-Strategy Iteration</b>, VMCAI'13 <br> <small> Peter Schrammel, Pavle Subotic</small> <small>(<a href=./papers/VMCAI13.pdf>paper</a>)</small></li>
</ol>
   </section>


  <h2>
<a id="intro" class="anchor" href="#intro" aria-hidden="true"><span aria-hidden="true" class="octicon octicon-link"></span></a>Technical Reports/Workshops/Abstracts</h2>
<ol>
<li><b>Beyond Deductive Datalog: How Datalog is used to perform AI tasks for program analysis, (Position Paper) LPOP'24,  <br> <small> Bernhard Scholz, Pavle Subotic and David Zhao </small> <small>(<a href=./papers/LPOP_Position_Paper_2024_2.pdf>paper</a>)</small></li>
<li><b>Towards Formal Verification of DAG-Based Blockchain Consensus Protocols (Extended Abstract) FMBC'24, <br> <small> Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotić </small> <small>(<a href=./papers/FMBC_abstract.pdf>paper</a>)</small> </li>
<li><b>Designing a Datalog Engine for Industrial-Grade Static Analysis, (Position Paper) LPOP'23,  <br> <small> Pavle Subotic and Bernhard Scholz </small> <small>(<a href=./papers/LPOP_Position_Paper.pdf>paper</a>, <a href=https://www.youtube.com/watch?v=mHVIdHLp9ZQ&t=1s>talk</a>)</small> </li>
<li><b>Rinser: Deriving Succinct Evidence for Automated Code Reviews</b>, (Invited Talk) Infer Practitioners@PLDI'20, <br> <small> Thanh-Toan Nguyen, Pavle Subotic, Bor-Yuh Evan Chang </small> <small>(<a href=./papers/CodeReviewBot.pdf>paper</a>, <a href=https://www.youtube.com/watch?v=FPCZ2TIxrpg&t=8888s>talk</a>)</small> </li>
<li><b>Incremental Datalog Prototype in Souffle</b>, (Extended Abstract) IC@SPLASH'19, <br> <small> David Zhao, Pavle Subotic, Bernhard Scholz </small>
<li><b>Static Analysis by Elimination</b>, Bytecode@ETAPS'13 <br> <small>Pavle Subotic, Andrew Santosa, Bernhard Scholz</small> <small>(<a href=./papers/BYTE13.pdf>paper</a>)</small></li>
<li><b>Enhancement of Teleconferencing Audio – Meta Information Extraction from Meeting Recordings. In Proc. CSIRO ICT Centre Conference'04, <br><small> Claudia Schremmer, Silvia Pfeiffer, Pavle Subotic, Eva Cheng </small>
</ol>
   </section>
  <h2>
<a id="intro" class="anchor" href="#intro" aria-hidden="true"><span aria-hidden="true" class="octicon octicon-link"></span></a>My Technical Blogs</h2>
<ol>
<li><b><a href=https://blog.soniclabs.com/an-inside-look-into-sonic-researchs-formal-model-driven-development-process/>Sonic Labs Formal Methods Process</a></li>
<li><b><a href=https://blog.soniclabs.com/soniccs-2-0-new-consensus-for-2x-faster-and-68-memory-reduction-2/>Sonic Consensus 2.0</a></li>
<li><b><a href=https://blog.soniclabs.com/beyond-audits-mathematically-verifying-the-safety-of-the-sonic-gateway/>Beyond Audits: Mathematically Verifying the Safety of the Sonic Gateway</a></li>
<li><b> <a href=https://blog.soniclabs.com/inside-sonicdb-faster-state-access-without-the-overhead/>Inside SonicDB: Faster State Access Without the Overhead</a></b></li>
</ol>
   </section>
    </div>
  </body>
</html>