FM24: 26TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

A
Abraham, Erika	A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
Adelt, Julius	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
Akshay, S.	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Aldinucci, Marco	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Ammar, Nejib	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
An, Jie	CauMon: An Informative Online Monitor for Signal Temporal Logic The Opacity of Timed Automata
Arcaini, Paolo	CauMon: An Informative Online Monitor for Signal Temporal Logic
B
Bae, Kyungmin	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
Baier, Daniel	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Baldauf, Jake Brandon	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Barbosa, Haniel	Satisfiability Modulo Theories: A Beginner's Tutorial
Bargmann, Lara	Unifying Weak Memory Verification using Potentials
Barrett, Clark	Satisfiability Modulo Theories: A Beginner's Tutorial The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
Barros, Ana Inês	Alloy repair hint generation based on historical data
Basin, David	Getting Chip Card Payments Right
Baumeister, Jan	A Tutorial on Stream-based Monitoring
Baumeister, Tom	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Baxter, James	RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first)
Beckert, Bernhard	The Java Verification Tool KeY: A Tutorial
Bergersen, Gunnar Rye	Stochastic Games for User Journeys
Beutner, Raven	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
Beyer, Dirk	Software Verification with CPAchecker 3.0: Tutorial and User Guide fm-weck: Containerized Execution of Formal Methods Tools
Blicha, Martin	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Bombarda, Andrea	ASMETA tool set for rigorous system design
Bonfanti, Silvia	ASMETA tool set for rigorous system design
Bono, Viviana	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Bordais, Benjamin	Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Bordis, Tabea	Free Facts: An Alternative to Inefficient Axioms in Dafny
Brain, Martin	The Pyramid Of (Formal) Software Verification
Britikov, Konstantin	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Bubel, Richard	The Java Verification Tool KeY: A Tutorial
Burns, Alan	Extending rely-guarantee thinking to handle real-time scheduling (Journal first)
Bury, Guillaume	Chamelon : a delta-debugger for OCaml
Busany, Nimrod	Fast Attack Graph Defense Localization via Bisimulation
C
Cai, Shaowei	A Local Search Algorithm for MaxSMT(LIA)
Calinescu, Radu	Code-level Safety Verification for Automated Driving: A Case Study
Carvalho, Gustavo	RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first)
Cavalcanti, Ana	Comparing Reactive Models and Cyclic Components of Robotic Systems: The RoboStar approach to model-based testin
Cavalcanti, Ana	RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first)
Chakraborty, Supratik	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Chambart, Pierre	Chamelon : a delta-debugger for OCaml
Chatterjee, Krishnendu	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Chen, Guangke	Certified Quantization Strategy Synthesis for Neural Networks
Chen, Mingshuai	Proving Functional Program Equivalence via Directed Lemma Synthesis
Chen, Taolue	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
Chien, Po-Chun	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Chin, Wei-Ngan	Staged Specification Logic for Verifying Higher-Order Imperative Programs
Colonnelli, Iacopo	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Cook, Byron	The Business of Proof Thoughts on the interplay between corporate, government, and university R&D
Coopmans, Tim	Advancing Quantum Computing with Formal Methods
Coughlin, Nicholas	Detecting speculative execution vulnerabilities on weak memory models
Courant, Nathanaëlle	Chamelon : a delta-debugger for OCaml
Cunha, Alcino	Alloy repair hint generation based on historical data
D
De Giacomo, Giuseppe	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Dedden, Frank	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Dell'Erba, Daniele	DFAMiner: Mining minimal separating DFAs from labelled samples
Deng, Weilin	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Di Stasio, Antonio	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Ding, Jianqiang	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Dong, Jin Song	Certified Quantization Strategy Synthesis for Neural Networks
Dong, Zhen	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
Dongol, Brijesh	Unifying Weak Memory Verification using Potentials
Drodt, Daniel	The Java Verification Tool KeY: A Tutorial
Dutta, Souradeep	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
E
Ehlers, Rüdiger	Understanding Synthesized Reactive Systems Through Invariants
Eichler, Paul	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
F
Fang, Jian	Proving Functional Program Equivalence via Directed Lemma Synthesis
Fang, Wang	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Fedyukovich, Grigory	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Fei, Yuan	FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First)
Feliu, Marco A.	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Fellowship Award, Fme	FME Fellowship Award
Feng, Shenghua	Switching Controller Synthesis for Hybrid Systems Against STL Formulas On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Finkbeiner, Bernd	A Tutorial on Stream-based Monitoring HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
Foo, Darius	Staged Specification Logic for Verifying Higher-Order Imperative Programs
Frohn, Florian	Integrating Loop Acceleration into Bounded Model Checking
Fu, Yubao	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
Furia, Carlo A.	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
G
Gan, Ting	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Ganlath, Akila	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Gao, Qiang	The Opacity of Timed Automata
Gargantini, Angelo	ASMETA tool set for rigorous system design
Garlan, David	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Geng, Yuang	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Gerasimou, Simos	Code-level Safety Verification for Automated Driving: A Case Study
Giesl, Jürgen	Integrating Loop Acceleration into Bounded Model Checking
Goodloe, Alwyn	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Goubault, Eric	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Govind, R.	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Greenman, Ben	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Gu, Rong	Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems (Journal first)
Gu, Yinyou	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
Guan, Ji	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Göbl, Angelina	HyGaViz: Visualizing Game-Based Certificates for Hyperproperty Verification
H
Hartmanns, Arnd	Efficient Formally Verified Maximal End Component Decomposition for MDPs
Hasuo, Ichiro	CauMon: An Informative Online Monitor for Signal Temporal Logic The Opacity of Timed Automata
He, Xiang	A Local Search Algorithm for MaxSMT(LIA)
Herber, Paula	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
Hofmeier, Xenia	Getting Chip Card Payments Right
Huang, Chao	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
Huang, Lin	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Hupel, Lars	Extending Isabelle/HOL’s Code Generator with support for the Go programming language
Hähnle, Reiner	The Java Verification Tool KeY: A Tutorial
I
Imrie, Calum	Code-level Safety Verification for Automated Driving: A Case Study
Inverso, Omar	Accurate Static Data Race Detection for C
J
Jacobs, Swen	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Jakobs, Marie-Christine	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Jankola, Marek	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Janota, Mikolas	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
Ji, Juntao	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
Ji, Ruyi	Proving Functional Program Equivalence via Directed Lemma Synthesis
Jiang, Xuanlin	Proving Functional Program Equivalence via Directed Lemma Synthesis
Johansson, Bjarne	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Johnsen, Einar Broch	Stochastic Games for User Journeys
Jones, Cliff	Extending rely-guarantee thinking to handle real-time scheduling (Journal first)
Jongmans, Sung-Shik	Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last
Junges, Sebastian	State Matching and Multiple References in Adaptive Active Automata Learning
K
Kafshdar Goharshady, Amir	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Kafshdar Goharshady, Ehsan	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Kang, Eunsuk	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Kapoor, Parv	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Karrabi, Mehrdad	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
Kettl, Matthias	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Klein, Dan	Fast Attack Graph Defense Localization via Bisimulation
Kobialka, Paul	Stochastic Games for User Journeys
Kohlen, Bram	Efficient Formally Verified Maximal End Component Decomposition for MDPs
Kohn, Florian	A Tutorial on Stream-based Monitoring
Kress-Gazit, Hadas	Formal Methods for Robotics and Human-Robot Interaction
Krishnamurthi, Shriram	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Kruger, Loes	State Matching and Multiple References in Adaptive Active Automata Learning
Kwiatkowska, Marta	Adversarial Robustness Certification for Bayesian Neural Networks Partially Observable Stochastic Games with Neural Perception Mechanisms
L
Laarman, Alfons	Advancing Quantum Computing with Formal Methods
Lam, Kait	Detecting speculative execution vulnerabilities on weak memory models
Lammich, Peter	Efficient Formally Verified Maximal End Component Decomposition for MDPs
Lanzinger, Florian	The Java Verification Tool KeY: A Tutorial
Laviron, Vincent	Chamelon : a delta-debugger for OCaml
Lecomte, Thierry	B+ or how to model system properties in a formal software model
Lee, Edward	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Lee, Jaeseo	Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption
Lee, Nian-Ze	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Leino, K. Rustan M.	Free Facts: An Alternative to Inefficient Axioms in Dafny
Lemberger, Thomas	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Leuschel, Michael	B2SAT: A Bare-Metal Reduction of B to SAT
Li, Bohan	A Local Search Algorithm for MaxSMT(LIA)
Li, Wei	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Li, Xiakun	Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Li, Yong	DFAMiner: Mining minimal separating DFAs from labelled samples
Liang, Zhen	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Lin, Qingshan	Beyond the Bottleneck: Enhancing High-Concurrency Systems with Lock Tuning
Lin, Yanling	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Lingsch-Rosenfeld, Marian	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Lopez Pombo, Carlos Gustavo	Automated Static Analysis of Quality of Service Properties of Communicating Systems
M
Macedo, Nuno	Alloy repair hint generation based on historical data
Manquinho, Vasco	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
Maoz, Shahar	Fast Attack Graph Defense Localization via Bisimulation
Marksteiner, Stefan	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Martina, Maurizio	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Martinez Suñé, Agustín Eloy	Automated Static Analysis of Quality of Service Properties of Communicating Systems
Masci, Paolo	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Medic, Doriana	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Mei, Jingyi	Advancing Quantum Computing with Formal Methods
Meira-Goes, Romulo	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Mensing, Robert Aron	Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid Systems
Mishra, Shatadal	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Moezkarimi, Zahra	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Monahan, Rosemary	Formalising Requirements for Systems Verification
Montali, Marco	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Moscato, Mariano	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Motwani, Harshit Jitendra	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Mulone, Alberto	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Munoz, Cesar	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Murray, Toby	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
N
Neider, Daniel	Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Nelson, Tim	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Nenchev, Vladislav	Code-level Safety Verification for Automated Driving: A Case Study
Neto, Henrique	Alloy repair hint generation based on historical data
Niemetz, Aina	Satisfiability Modulo Theories: A Beginner's Tutorial
Norman, Gethin	Partially Observable Stochastic Games with Neural Perception Mechanisms
O
Ohrimenko, Olga	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
Organizers, Fm	FM24 Opening Industry partner pitches
Orvalho, Pedro	CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases
P
Padovani, Luca	Introducing SWIRL: An Intermediate Representation Language for Scientific Workflows
Paiva, Ana C. R.	Alloy repair hint generation based on historical data
Papadopoulos, Alessandro	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Parker, David	Partially Observable Stochastic Games with Neural Perception Mechanisms
Pereira, Mário	Practical Deductive Verification of OCaml Programs
Perez, Ivan	Runtime Verification in Real-Time with the Copilot Language: A Tutorial
Pfeifer, Wolfram	The Java Verification Tool KeY: A Tutorial
Pferscher, Andrea	Stochastic Games for User Journeys
Pham, Van-Thuan	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
Polgreen, Elizabeth	The Pyramid Of (Formal) Software Verification
Pourvatan, Bahman	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Prakash, Jyoti	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
Prasad, Siddhartha	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Preiner, Mathias	Satisfiability Modulo Theories: A Beginner's Tutorial
Promies, Valentin	A Divide-and-Conquer Approach to Variable Elimination in Linear Real Arithmetic
Przybocki, Benjamin	The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
Putot, Sylvie	A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
Q
Quist, Arend-Jan	Advancing Quantum Computing with Formal Methods
R
Raia, Gaetano	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Reynolds, Andrew	Satisfiability Modulo Theories: A Beginner's Tutorial
Riccobene, Elvinia	ASMETA tool set for rigorous system design
Rigano, Gianluca	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Rodrigues Júnior, Francisco	RoboWorld: Verification of Robotic Systems with Environment in the Loop (Journal first)
Rot, Jurriaan	State Matching and Multiple References in Adaptive Active Automata Learning
Roy, Rajarshi	Learning Branching-Time Properties in CTL and ATL via Constraint Solving
Rozier, Kristin-Yvonne	On Time and Space (Of Humans)
Ruchkin, Ivan	Bridging Dimensions: Confident Reachability for High-Dimensional Controllers
S
Sakr, Mouhammad	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
Sales, Emerson	Accurate Static Data Race Detection for C
Santos, Gabriel	Partially Observable Stochastic Games with Neural Perception Mechanisms
Sasse, Ralf	Getting Chip Card Payments Right
Scandurra, Patrizia	ASMETA tool set for rigorous system design
Scheerer, Frederik	A Tutorial on Stream-based Monitoring
Schewe, Sven	DFAMiner: Mining minimal separating DFAs from labelled samples
Shalom, Rafi	Fast Attack Graph Defense Localization via Bisimulation
Sharygina, Natasha	Reachability Analysis for Multiloop Programs Using Transition Power Abstraction
Sirjani, Marjan	Systematic Test Case Generation for Distributed Redundant Controllers using Model Checking (EXTENDED ABSTRACT)
Sison, Robert	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
Smith, Graeme	Detecting speculative execution vulnerabilities on weak memory models
Song, Fu	Certified Quantization Strategy Synthesis for Neural Networks Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
Song, Yahui	Staged Specification Logic for Verifying Higher-Order Imperative Programs
Stoelinga, Marielle	No risk, no fun: a tutorial on risk management
Stübinger, Terru	Extending Isabelle/HOL’s Code Generator with support for the Go programming language
Su, Han	Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Su, Zhaofeng	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Sun, Jun	Certified Quantization Strategy Synthesis for Neural Networks
Sun, Yican	Proving Functional Program Equivalence via Directed Lemma Synthesis
T
Tan, Huiyu	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
Tapia Tarifa, Silvia Lizeth	Stochastic Games for User Journeys
Tinelli, Cesare	Satisfiability Modulo Theories: A Beginner's Tutorial
Titolo, Laura	Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Tiwari, Abhishek	Automated Repair of Information Flow Security in Android Implicit Inter-App Communication
Toledo, Guilherme	The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
Toro-Pozo, Jorge	Getting Chip Card Payments Right
Tuosto, Emilio	Accurate Static Data Race Detection for C Automated Static Analysis of Quality of Service Properties of Communicating Systems
U
Ulbrich, Mattias	The Java Verification Tool KeY: A Tutorial
V
Valnet, Milla	Chamelon : a delta-debugger for OCaml
Varanasi, Sai Teja	Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic
Vincenzoni, David	Employing Formal Equivalence Methods to Ensure Correspondence between a High-Level C/C++ Model and its RTL Design
Völp, Marcus	Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata
W
Wachowitz, Henrik	Software Verification with CPAchecker 3.0: Tutorial and User Guide fm-weck: Containerized Execution of Formal Methods Tools
Wang, Hanfeng	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Wang, Jie	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Wang, Lingtai	The Opacity of Timed Automata
Wang, Minghua	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Wang, Xilong	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Wehrheim, Heike	Unifying Weak Memory Verification using Potentials
Wei, Tao	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Weigl, Alexander	The Java Verification Tool KeY: A Tutorial
Wendler, Philipp	Software Verification with CPAchecker 3.0: Tutorial and User Guide
Winter, Kirsten	Detecting speculative execution vulnerabilities on weak memory models
Wu, Hao	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Wu, Taoran	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Wu, Zhilin	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
X
Xia, Bican	On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Xie, Ningning	Safe and Easy Compile-Time Generative Programming
Xiong, Yingfei	Proving Functional Program Equivalence via Directed Lemma Synthesis
Xue, Bai	PyBDR: Set-boundary based Reachability Analysis Toolkit in Python
Xue, Jingling	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Y
Yan, Pengbo	Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms
Yan, Rui	Partially Observable Stochastic Games with Neural Perception Mechanisms
Yang, Xi	Compositional Verification of Cryptographic Circuits against Fault Injection Attacks
Yang, Zhibin	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Yin, Jiaqi	FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First)
Ying, Mingsheng	VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models
Z
Zhan, Naijun	Switching Controller Synthesis for Hybrid Systems Against STL Formulas On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains The Opacity of Timed Automata Nonlinear Craig Interpolant Generation over Unbounded Domains by Separating Semialgebraic Sets
Zhan, Sinong	Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Zhang, Changjian	Tolerance of Reinforcement Learning Controllers against Deviations in Cyber Physical Systems
Zhang, Yedi	Certified Quantization Strategy Synthesis for Neural Networks
Zhang, Zhenya	CauMon: An Informative Online Monitor for Signal Temporal Logic
Zhao, Mengyu	A Local Search Algorithm for MaxSMT(LIA)
Zhou, Yong	AGVTS: Automated Generation and Verification of Temporal Specifications for Aeronautics SCADE Models
Zhu, Huibiao	FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT (Journal First)
Zhu, Shufang	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Zi, Yuan	UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Zizyte, Milda	Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic
Zohar, Yoni	Satisfiability Modulo Theories: A Beginner's Tutorial The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems
Ž
Žikelić, Ðorđe	Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs

Disclaimer | Powered by EasyChair Smart Program