publications

2025

1. POPL 2025

   Reachability Analysis of the Domain Name System

   Dhruv Nevatia^†, Si Liu, and David Basin

   Proc. ACM Program. Lang., 2025

   Abs

   TBA

2024

1. OOPSLA 2024

   Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels

   Si Liu, Long Gu, Hengfeng Wei, and David Basin

   Proc. ACM Program. Lang., 2024

   Abs

   Modern databases embrace weak isolation levels to cater for highly available transactions. However, weak isolation bugs have recently manifested in many production databases. This raises the concern of whether database implementations actually deliver their promised isolation guarantees in practice. In this paper we present Plume, the first efficient, complete, black-box checker for weak isolation levels. Plume builds on modular, fine-grained transactional anomalous patterns, with which we establish sound and complete characterizations of representative weak isolation levels, including read committed, read atomicity, and transactional causal consistency. Plume leverages a novel combination of two techniques, vectors and tree clocks, to accelerate isolation checking. Our extensive assessment shows that Plume can reproduce all known violations in a large collection of anomalous database execution histories, detect new isolation bugs in three production databases along with informative counterexamples, find more weak isolation anomalies than the state-of-the-art checkers, and efficiently validate isolation guarantees under a wide variety of workloads.

2. SIGMOD 2024

   NOC-NOC: Towards Performance-optimal Distributed Transactions

   Si Liu, Luca Multazzu, Hengfeng Wei, and David Basin

   Proc. ACM Manag. Data, 2024

   Abs

   Substantial research efforts have been devoted to studying the performance optimality problem for distributed database transactions. However, they focus just on optimizing transactional reads, and thus overlook crucial factors, such as the efficiency of writes, which also impact the overall system performance. Motivated by a recent study on Twitter’s workloads showing the prominence of write-heavy workloads in practice, we make a substantial step towards performance-optimal distributed transactions by also aiming to optimize writes, a fundamentally new dimension to this problem. We propose a new design objective and establish impossibility results with respect to the achievable isolation levels. Guided by these results, we present two new transaction algorithms with different isolation guarantees that fulfill this design objective. Our evaluation demonstrates that these algorithms outperform the state of the art.

3. VLDB 2024 Demo

   IsoVista: Black-box Checking Database Isolation Guarantees

   Long Gu^†, Si Liu, Tiancheng Xing, Hengfeng Wei, Yuxing Chen, and David Basin

   Proc. VLDB Endow., 2024

   Abs

   Transactional isolation is critical to the functional correctness of database management systems (DBMSs). Much effort has recently been devoted to finding isolation bugs and validating isolation fulfilment in production DBMSs. However, there are still challenges that existing isolation checkers have not yet fully addressed. For instance, they may overlook bugs, incur high checking overhead, and return hard-to-understand counterexamples. We present IsoVista, the first black-box isolation checking system that encompasses all the following features. It builds on faithful characterizations of a range of isolation levels, ensuring the absence of both false positives and missed bugs in collected DBMS execution histories. IsoVista exhibits superior checking efficiency, compared to the state-of-the-art, and visualizes violation scenarios, facilitating the understanding of bugs found. It also supports profiling and benchmarking the performance of isolation checkers under various workloads, assisting developers of both DBMSs and checkers. We showcase all these features through user-friendly interfaces

4. USENIX SEC 2024

   CAMP: Compositional Amplification Attacks against DNS

   Huayi Duan, Marco Bearzi, Jodok Vieli, David Basin, Adrian Perrig, Si Liu, and Bernhard Tellenbach

   In 33rd USENIX Security Symposium (USENIX Security 24), 2024

   Abs

   While DNS is often exploited by reflective DoS attacks, it can also be weaponized as a powerful amplifier to overload itself, as evidenced by a stream of recently discovered application-layer amplification attacks. Given the importance of DNS, the question arises of what the fundamental traits are for such attacks. To answer this question, we perform a systematic investigation by establishing a taxonomy of amplification primitives intrinsic to DNS and a framework to analyze their composability. This approach leads to the discovery of a large family of compositional amplification (CAMP) vulnerabilities, which can produce multiplicative effects with message amplification factors of hundreds to thousands. Our measurements with popular DNS implementations and open resolvers indicate the ubiquity and severity of CAMP vulnerabilities and the serious threats they pose to the Internet’s crucial naming infrastructure.

5. CAV 2024

   Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems

   Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong, and Min Zhang

   In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II, 2024

   Abs

   The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs). This underscores the pressing need to promptly establish certified safety guarantees for such DNN-controlled systems. Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. However, qualitative verification proves inadequate for DNN-controlled systems as their behaviors exhibit stochastic tendencies when operating in open and adversarial environments. In this paper, we propose a novel framework for unifying both qualitative and quantitative safety verification problems of DNN-controlled systems. This is achieved by formulating the verification tasks as the synthesis of valid neural barrier certificates (NBCs). Initially, the framework seeks to establish almost-sure safety guarantees through qualitative verification. In cases where qualitative verification fails, our quantitative verification method is invoked, yielding precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons. To facilitate the synthesis of NBCs, we introduce their k-inductive variants. We also devise a simulation-guided approach for training NBCs, aiming to achieve tightness in computing precise certified lower and upper bounds. We prototype our approach into a tool called and showcase its efficacy on four classic DNN-controlled systems.

6. VMCAI 2024

   Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training

   Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Guy Katz, and Min Zhang

   In Verification, Model Checking, and Abstract Interpretation: 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part II, London, United Kingdom, 2024

   Abs

   The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted to specific types of DNNs. This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. Specifically, we extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. The inserted abstraction layer ensures that the values represented by an interval are indistinguishable to the network for both training and decision-making. Leveraging this, we devise the first black-box reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states. Our approach is sound, tight, efficient, and agnostic to any DNN type and size. The experimental results on a wide range of benchmarks show that the DNNs trained by using our approach exhibit comparable performance, while the reachability analysis of the corresponding systems becomes more amenable with significant tightness and efficiency improvement over the state-of-the-art white-box approaches.

2023

1. VLDB 2023

   Efficient Black-box Checking of Snapshot Isolation in Databases

   Si Liu^*, Kaile Huang^*, Zhenge Chen, Hengfeng Wei, David Basin, Haixiang Li, and Anqun Pan

   Proc. VLDB Endow., 2023

   Abs

   Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomalies. Nevertheless, SI anomalies have recently been found in production cloud databases that claim to provide the SI guarantee. Given the complex and often unavailable internals of such databases, a black-box SI checker is highly desirable. In this paper we present PolySI, a black-box checker that efciently checks SI and provides understandable counterexamples upon detecting violations. PolySI builds on a characterization of SI using generalized polygraphs (GPs), for which we establish its soundness and completeness. PolySI employs an SMT solver and also accelerates SMT solving by utilizing a compact constraint encoding of GPs and domain-specifc optimizations for pruning constraints. As our extensive assessment demonstrates, PolySI successfully reproduces all of 2477 known SI anomalies, detects novel SI violations in three production cloud databases, identifes their causes, outperforms the state-of-the-art black-box checkers under a wide range of workloads, and can scale up to large workloads.

2. OSDI 2023

   Detecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction

   Zu-Ming Jiang, Si Liu, Manuel Rigger, and Zhendong Su

   In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23), 2023

   Abs

   Transactions are an important feature of database management systems (DBMSs), as they provide the ACID guarantees for a sequence of database operations. Consequently, approaches have been proposed to automatically find transactional bugs in DBMSs. However, they cannot handle complex operations and predicates common in real-world database queries, and thus miss bugs. This paper introduces a general, effective technique for finding transactional bugs in DBMSs that supports complex SQL queries and predicates. At the conceptual level, we address the test-oracle problem by constructing semantically-equivalent test cases based on fine-grained statement-level dependencies in transactions. At the technical level, we introduce (1) statement-dependency graphs to describe dependencies among SQL statements in transactions, (2) SQL-level instrumentation to capture possible statement-level dependencies, and (3) transactional oracle construction to generate semantically-equivalent test cases using statement-dependency graphs. We also establish the correctness of our approach in generating semantically-equivalent test cases. We have realized our technique as a tool, TxCheck, and evaluated it on three widely-used and well-tested DBMSs, namely TiDB, MySQL, and MariaDB. In total, TxCheck found 56 unique bugs, 52 of which have been confirmed and 18 already fixed. We believe that TxCheck can help solidify DBMSs’ support for transactions thanks to its generality and effectiveness.

3. SIGCOMM 2023

   A Formal Framework for End-to-End DNS Resolution

   Si Liu, Huayi Duan, Lukas Heimes, Marco Bearzi, Jodok Vieli, David Basin, and Adrian Perrig

   In Proceedings of the ACM SIGCOMM 2023 Conference, New York, NY, USA, 2023

   Abs

   Despite the central importance of DNS, numerous attacks and vulnerabilities are regularly discovered. The root of the problem is the ambiguity and tremendous complexity of DNS protocol specifications, amid a rapidly evolving Internet infrastructure. To counteract the vicious break-and-fix cycle for improving DNS infrastructure, we instigate a foundational approach: we construct the first formal semantics of end-to-end name resolution, a collection of components for the formal analyses of both qualitative and quantitative properties, and an automated tool for discovering DoS attacks. Our formal framework represents an important step towards a substantially more secure and reliable DNS infrastructure.

4. NSDI 2023

   RHINE: Robust and High-performance Internet Naming with E2E Authenticity

   Huayi Duan, Rubén Fischer, Jie Lou, Si Liu, David Basin, and Adrian Perrig

   In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), 2023

   Abs

   The variety and severity of recent DNS-based attacks under- score the importance of a secure naming system. Although DNSSEC provides data authenticity in theory, practical deployments unfortunately are fragile, costly, and typically lacks end-to-end (E2E) guarantees. This motivates us to rethink authentication in DNS fundamentally and introduce RHINE, a secure-by-design Internet naming system. RHINE offloads the authentication of zone delegation to an end-entity PKI and tames the operational complexity in an offline manner, allowing the efficient E2E authentication of zone data during online name resolution. With a novel logging mechanism, Delegation Transparency, RHINE achieves a highly robust trust model that can tolerate the compromise of all but one trusted entities and, for the first time, counters threats from superordinate zones. We formally verify RHINE’s security properties using the Tamarin prover. We also demonstrate its practicality and performance advantages with a prototype implementation.

5. NeurIPS 2023

   Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural Networks

   Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Cheng Chen, and Min Zhang

   In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023

   Abs

   Formally verifying deep reinforcement learning (DRL) systems suffers from both inaccurate verification results and limited scalability. The major obstacle lies in the large overestimation introduced inherently during training and then transforming the inexplicable decision-making models, i.e., deep neural networks (DNNs), into easy-to-verify models. In this paper, we propose an inverse transform-then-train approach, which first encodes a DNN into an equivalent set of efficiently and tightly verifiable linear control policies and then optimizes them via reinforcement learning. We accompany our inverse approach with a novel neural network model called piece-wise linear decision neural networks (PLDNNs), which are compatible with most existing DRL training algorithms with comparable performance against conventional DNNs. Our extensive experiments show that, compared to DNN-based DRL systems, PLDNN-based systems can be more efficiently and tightly verified with up to 438 times speedup and a significant reduction in overestimation. In particular, even a complex 12-dimensional DRL system is efficiently verified with up to 7 times deeper computation steps.

6. CVPR 2023

   Boosting Verified Training for Robust Image Classifications via Abstraction

   Zhaodi Zhang, Zhiyi Xue, Yang Chen, Si Liu, Yueling Zhang, Jing Liu, and Min Zhang

   In IEEE/CVF Conference on Computer Vision and Pattern Recognition, CVPR 2023, Vancouver, BC, Canada, June 17-24, 2023, 2023

   Abs

   This paper proposes a novel, abstraction-based, certified training method for robust image classifiers. Via abstraction, all perturbed images are mapped into intervals before feeding into neural networks for training. By training on intervals, all the perturbed images that are mapped to the same interval are classified as the same label, rendering the variance of training sets to be small and the loss landscape of the models to be smooth. Consequently, our approach significantly improves the robustness of trained models. For the abstraction, our training method also enables a sound and complete black-box verification approach, which is orthogonal and scalable to arbitrary types of neural networks regardless of their sizes and architectures. We evaluate our method on a wide range of benchmarks in different scales. The experimental results show that our method outperforms state of the art by (i) reducing the verified errors of trained models up to 95.64%; (ii) totally achieving up to 602.50x speedup; and (iii) scaling up to larger models with up to 138 million trainable parameters. The demo is available at https://github.com/zhangzhaodi233/ABSCERT.git.

7. ISSTA 2023

   A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation

   Zhiyi Xue, Si Liu, Zhaodi Zhang, Yiting Wu, and Min Zhang

   In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, Seattle, WA, USA, 2023

   Abs

   The robustness of deep neural networks (DNNs) is crucial to the hosting system’s reliability and security. Formal verification has been demonstrated to be effective in providing provable robustness guarantees. To improve its scalability, over-approximating the non-linear activation functions in DNNs by linear constraints has been widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. Many efforts have been dedicated to defining the so-called tightest approximations to reduce overestimation imposed by over-approximation. In this paper, we study existing approaches and identify a dominant factor in defining tight approximation, namely the approximation domain of the activation function. We find out that tight approximations defined on approximation domains may not be as tight as the ones on their actual domains, yet existing approaches all rely only on approximation domains. Based on this observation, we propose a novel dual-approximation approach to tighten overapproximations, leveraging an activation function’s underestimated domain to define tight approximation bounds. We implement our approach with two complementary algorithms based respectively on Monte Carlo simulation and gradient descent into a tool called DualApp. We assess it on a comprehensive benchmark of DNNs with different architectures. Our experimental results show that DualApp significantly outperforms the state-of-the-art approaches with 100% − 1000% improvement on the verified robustness ratio and 10.64% on average (up to 66.53%) on the certified lower bound.

2022

1. OOPSLA 2022

   Bridging the semantic gap between qualitative and quantitative models of distributed systems

   Si Liu, Jose Meseguer, Peter Csaba Ölveczky, Min Zhang, and David Basin

   Proc. ACM Program. Lang., Oct 2022

   Abs

   Today’s distributed systems must satisfy both qualitative and quantitative properties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare/separation logics, for qualitative properties; and timed/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible to represent intrinsic features of distributed object systems—such as unbounded data structures, dynamic object creation, and an unbounded number of messages—using finite automata. In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha’s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into the Actors2PMaude tool. We illustrate the expressiveness of our framework and our tool’s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs—including an industrial data store and a state-of-the-art transaction system—into quantitative models to analyze and compare the performance of different designs.

2. TOSEM 2022

   All in One: Design, Verification, and Implementation of SNOW-optimal Read Atomic Transactions

   Si Liu

   ACM Trans. Softw. Eng. Methodol., Mar 2022

   Abs

   Distributed read atomic transactions are important building blocks of modern cloud databases that magnificently bridge the gap between data availability and strong data consistency. The performance of their transactional reads is particularly critical to the overall system performance, as many real-world database workloads are dominated by reads. Following the SNOW design principle for optimal reads, we develop LORA, a novel SNOW-optimal algorithm for distributed read atomic transactions. LORA completes its reads in exactly one round trip, even in the presence of conflicting writes, without imposing additional overhead to the communication, and it outperforms the state-of-the-art read atomic algorithms.To guide LORA’s development, we present a rewriting-logic-based framework and toolkit for design, verification, implementation, and evaluation of distributed databases. Within the framework, we formalize LORA and mathematically prove its data consistency guarantees. We also apply automatic model checking and statistical verification to validate our proofs and to estimate LORA’s performance. We additionally generate from the formal model a correct-by-construction distributed implementation for testing and performance evaluation under realistic deployments. Our design-level and implementation-based experimental results are consistent, which together demonstrate LORA’s promising data consistency and performance achievement.

3. CSF 2022

   N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures

   Thilo Weghorn, Si Liu^*, Christoph Sprenger, Adrian Perrig, and David Basin

   In 2022 IEEE 35th Computer Security Foundations Symposium (CSF), Mar 2022

   Abs

   We present N-Tube, a novel, provably secure, inter-domain bandwidth reservation algorithm that runs on a network architecture supporting path-based forwarding. N-Tube reserves global end-to-end bandwidth along network paths in a distributed, neighbor-based, and tube-fair way. It guarantees that benign bandwidth demands are granted available allocations that are immutable, stable, lower-bounded, andfair, even during adversarial demand bursts. We formalize N-Tube and powerful adversaries as a labeled transition system, and inductively prove its safety and security properties. We also apply statistical model checking to validate our proofs and perform an additional quantitative assessment of N-Tube, providing strong guarantees for protection against DDoS attacks. We are not aware of any other complex networked system designs that have been subjected to a comparable analysis of both their qualitative properties (such as correctness and security) and their quantitative properties (such as performance).

4. Book Chapter

   Design-Level Verification

   David Basin, Tobias Klenze, Si Liu, and Christoph Sprenger

   Mar 2022
5. Book Chapter

   Extensions for the Data Plane

   Giacomo Giuliari, Markus Legner, Si Liu, Adrian Perrig, Thilo Weghorn, and Marc Wyss

   Mar 2022
6. ASE 2022

   Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks

   Zhaodi Zhang, Yiting Wu, Si Liu, Jing Liu, and Min Zhang

   In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, Rochester, MI, USA, Mar 2022

   Abs

   The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

2021

1. TASE 2021

   Exploring Design Alternatives for Replicated RAMP Transactions Using Maude

   Lei Liang, and Si Liu

   In 2021 International Symposium on Theoretical Aspects of Software Engineering (TASE), Mar 2021

2020

1. NFM 2020

   Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs

   Si Liu, Atul Sandur, José Meseguer, Peter Csaba Ölveczky, and Qi Wang

   In NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings, Mar 2020

2019

1. TACAS 2019

   Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude

   Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, and José Meseguer

   In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, Mar 2019
2. FAoC 2019

   Read atomic transactions with prevention of lost updates: ROLA and its formal analysis

   Si Liu, Peter Csaba Ölveczky, Qi Wang, Indranil Gupta, and José Meseguer

   Formal Aspects Comput., Mar 2019
3. CCS 2019

   Charting the Attack Surface of Trigger-Action IoT Platforms

   Qi Wang, Pubali Datta, Wei Yang, Si Liu, Adam Bates, and Carl A. Gunter

   In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, Mar 2019
4. PhD Thesis

   Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude

   Si Liu

   University of Illinois Urbana-Champaign, USA, Mar 2019

2018

1. FASE 2018

   ROLA: A New Distributed Transaction Protocol and Its Formal Analysis

   Si Liu, Peter Csaba Ölveczky, Keshav Santhanam, Qi Wang, Indranil Gupta, and José Meseguer

   In Fundamental Approaches to Software Engineering, 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Mar 2018
2. WRLA 2018

   Formal Modeling and Analysis of the Walter Transactional Data Store

   Si Liu, Peter Csaba Ölveczky, Qi Wang, and José Meseguer

   In Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings, Mar 2018
3. Book Chapter

   Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude

   Rakesh Bobba, Jon Grov, Indranil Gupta, Si Liu, José Meseguer, Peter Csaba Ölveczky, and Stephen Skeirik

   Mar 2018

2017

1. LITES 2017

   Quantitative Analysis of Consistency in NoSQL Key-Value Stores

   Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, and José Meseguer

   Leibniz Trans. Embed. Syst., Mar 2017
2. ICFEM 2017

   Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking

   Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, and José Meseguer

   In Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi’an, China, November 13-17, 2017, Proceedings, Mar 2017

2016

1. JLAMP 2016

   Modeling and analyzing mobile ad hoc networks in Real-Time Maude

   Si Liu, Peter Csaba Ölveczky, and José Meseguer

   J. Log. Algebraic Methods Program., Mar 2016
2. SAC 2016

   Formal modeling and analysis of RAMP transaction systems

   Si Liu, Peter Csaba Ölveczky, Muntasir Raihan Rahman, Jatin Ganhotra, Indranil Gupta, and José Meseguer

   In Proceedings of the 31st Annual ACM Symposium on Applied Computing, Pisa, Italy, April 4-8, 2016, Mar 2016

2015

1. SSS 2015

   Formal Analysis of Leader Election in MANETs Using Real-Time Maude

   Si Liu, Peter Csaba Ölveczky, and José Meseguer

   In Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, Mar 2015
2. QEST 2015

   Quantitative Analysis of Consistency in NoSQL Key-Value Stores

   Si Liu, Son Nguyen, Jatin Ganhotra, Muntasir Raihan Rahman, Indranil Gupta, and José Meseguer

   In Quantitative Evaluation of Systems, 12th International Conference, QEST 2015, Madrid, Spain, September 1-3, 2015, Proceedings, Mar 2015

2014

1. ICFEM 2014

   Formal Modeling and Analysis of Cassandra in Maude

   Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, and José Meseguer

   In Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, Mar 2014
2. WRLA 2014

   A Framework for Mobile Ad hoc Networks in Real-Time Maude

   Si Liu, Peter Csaba Ölveczky, and José Meseguer

   In Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers, Mar 2014
3. PRDC 2014

   Reasoning about Group-Based Mobility in MANETs

   Xi Wu, Si Liu, Huibiao Zhu, and Yongxin Zhao

   In 20th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2014, Singapore, November 18-21, 2014, Mar 2014

2013

1. ComSIS 2013

   Modeling and verifying the Ariadne protocol using process algebra

   Xi Wu, Huibiao Zhu, Yongxin Zhao, Zheng Wang, and Si Liu

   Comput. Sci. Inf. Syst., Mar 2013

2012

1. ECBS 2012

   Modeling and Verifying the Ariadne Protocol Using CSP

   Xi Wu, Si Liu, Huibiao Zhu, Yongxin Zhao, and Lei Chen

   In IEEE 19th International Conference and Workshops on Engineering of Computer-Based Systems, ECBS 2012, Novi Sad, Serbia, April 11-13, 2012, Mar 2012

2011

1. HASE 2011

   A Calculus for Mobile Ad Hoc Networks from a Group Probabilistic Perspective

   Si Liu, Yongxin Zhao, Huibiao Zhu, and Qin Li

   In 13th IEEE International Symposium on High-Assurance Systems Engineering, HASE 2011, Boca Raton, FL, USA, November 10-12, 2011, Mar 2011
2. ICECCS 2011

   Formal Model of Interrupt Program from a Probabilistic Perspective

   Yongxin Zhao, Yanhong Huang, Jifeng He, and Si Liu

   In 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27-29 April 2011, Mar 2011
3. SSIRI 2011

   Formal Approaches to Wireless Sensor Networks

   Si Liu, Xiaofeng Wu, Qin Li, Huibiao Zhu, and Qian Wang

   In Fifth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011, 27-29 June, 2011, Jeju Island, Korea - Companion Volume, Mar 2011
4. SSIRI 2011

   Towards Denotational Semantics for Verilog in PVS

   Han Zhu, Huibiao Zhu, Si Liu, and Jian Guo

   In Fifth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011, 27-29 June, 2011, Jeju Island, Korea - Companion Volume, Mar 2011
5. TASE 2011

   Towards a Probabilistic Calculus for Mobile Ad Hoc Networks

   Si Liu, Yongxin Zhao, Huibiao Zhu, and Qin Li

   In 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi’an, China, 29-31 August 2011, Mar 2011
6. TASE 2011

   Modeling and Analyzing the (mu)TESLA Protocol Using CSP

   Mengying Wang, Huibiao Zhu, Yongxin Zhao, and Si Liu

   In 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi’an, China, 29-31 August 2011, Mar 2011

2010

1. UTP 2010

   Promoting Models

   Qin Li, Yongxin Zhao, Xiaofeng Wu, and Si Liu

   In Unifying Theories of Programming - Third International Symposium, UTP 2010, Shanghai, China, November 15-16, 2010. Proceedings, Mar 2010