Showing 1–28 of 28 results for author: Liu, Y A

Applications of Machine Learning to Optimizing Polyolefin Manufacturing

Authors: Niket Sharma, Y. A. Liu

Abstract: This chapter is a preprint from our book by , focusing on leveraging machine learning (ML) in chemical and polyolefin manufacturing optimization. It's crafted for both novices and seasoned professionals keen on the latest ML applications in chemical processes. We trace the evolution of AI and ML in chemical industries, delineate core ML components, and provide resources for ML beginners. A detaile… ▽ More This chapter is a preprint from our book by , focusing on leveraging machine learning (ML) in chemical and polyolefin manufacturing optimization. It's crafted for both novices and seasoned professionals keen on the latest ML applications in chemical processes. We trace the evolution of AI and ML in chemical industries, delineate core ML components, and provide resources for ML beginners. A detailed discussion on various ML methods is presented, covering regression, classification, and unsupervised learning techniques, with performance metrics and examples. Ensemble methods, deep learning networks, including MLP, DNNs, RNNs, CNNs, and transformers, are explored for their growing role in chemical applications. Practical workshops guide readers through predictive modeling using advanced ML algorithms. The chapter culminates with insights into science-guided ML, advocating for a hybrid approach that enhances model accuracy. The extensive bibliography offers resources for further research and practical implementation. This chapter aims to be a thorough primer on ML's practical application in chemical engineering, particularly for polyolefin production, and sets the stage for continued learning in subsequent chapters. Please cite the original work [169,170] when referencing. △ Less

Submitted 18 January, 2024; originally announced January 2024.

Incremental Computation: What Is the Essence?

Authors: Yanhong A. Liu

Abstract: Incremental computation aims to compute more efficiently on changed input by reusing previously computed results. We give a high-level overview of works on incremental computation, and highlight the essence underlying all of them, which we call incrementalization -- the discrete counterpart of differentiation in calculus. We review the gist of a systematic method for incrementalization, and a syst… ▽ More Incremental computation aims to compute more efficiently on changed input by reusing previously computed results. We give a high-level overview of works on incremental computation, and highlight the essence underlying all of them, which we call incrementalization -- the discrete counterpart of differentiation in calculus. We review the gist of a systematic method for incrementalization, and a systematic method centered around it, called Iterate-Incrementalize-Implement, for program design and optimization, as well as algorithm design and optimization. At a meta-level, with historical contexts and for future directions, we stress the power of high-level data, control, and module abstractions in develo** new and better algorithms and programs as well as their precise complexities. △ Less

Submitted 13 December, 2023; originally announced December 2023.

Benchmarking for Integrating Logic Rules with Everything Else

Authors: Yanhong A. Liu, Scott D. Stoller, Yi Tong, K. Tuncay Tekle

Abstract: Integrating logic rules with other language features is increasingly sought after for advanced applications that require knowledge-base capabilities. To address this demand, increasingly more languages and extensions for such integration have been developed. How to evaluate such languages? This paper describes a set of programming and performance benchmarks for evaluating languages supporting… ▽ More Integrating logic rules with other language features is increasingly sought after for advanced applications that require knowledge-base capabilities. To address this demand, increasingly more languages and extensions for such integration have been developed. How to evaluate such languages? This paper describes a set of programming and performance benchmarks for evaluating languages supporting integrated use of rules and other features, and the results of evaluating such an integrated language together with logic languages and languages not supporting logic rules. △ Less

Submitted 30 August, 2023; originally announced August 2023.

Comments: In Proceedings ICLP 2023, arXiv:2308.14898. arXiv admin note: substantial text overlap with arXiv:2205.15204

Journal ref: EPTCS 385, 2023, pp. 12-26

Integrating Logic Rules with Everything Else, Seamlessly

Authors: Yanhong A. Liu, Scott D. Stoller, Yi Tong, Bo Lin

Abstract: This paper presents a language, Alda, that supports all of logic rules, sets, functions, updates, and objects as seamlessly integrated built-ins. The key idea is to support predicates in rules as set-valued variables that can be used and updated in any scope, and support queries using rules as either explicit or implicit automatic calls to an inference function. We have defined a formal semantic… ▽ More This paper presents a language, Alda, that supports all of logic rules, sets, functions, updates, and objects as seamlessly integrated built-ins. The key idea is to support predicates in rules as set-valued variables that can be used and updated in any scope, and support queries using rules as either explicit or implicit automatic calls to an inference function. We have defined a formal semantics of the language, implemented a prototype compiler that builds on an object-oriented language that supports concurrent and distributed programming and on an efficient logic rule system, and successfully used the language and implementation on benchmarks and problems from a wide variety of application domains. We describe the compilation method and results of experimental evaluation. △ Less

Submitted 30 May, 2023; originally announced May 2023.

Comments: To be published in Theory and Practice of Logic Programming, Special issue for selected papers from 39nd International Conference on Logic Programming. arXiv admin note: substantial text overlap with arXiv:2205.15204

Specification and Runtime Checking of Derecho, A Protocol for Fast Replication for Cloud Services

Authors: Kumar Shivam, Vishnu Paladugu, Yanhong A. Liu

Abstract: Reliable distributed systems require replication and consensus among distributed processes to tolerate process and communication failures. Understanding and assuring the correctness of protocols for replication and consensus have been a significant challenge. This paper describes the precise specification and runtime checking of Derecho, a more recent, sophisticated protocol for fast replication a… ▽ More Reliable distributed systems require replication and consensus among distributed processes to tolerate process and communication failures. Understanding and assuring the correctness of protocols for replication and consensus have been a significant challenge. This paper describes the precise specification and runtime checking of Derecho, a more recent, sophisticated protocol for fast replication and consensus for cloud services. A precise specification must fill in missing details and resolve ambiguities in English and pseudocode algorithm descriptions while also faithfully following the descriptions. To help check the correctness of the protocol, we also performed careful manual analysis and increasingly systematic runtime checking. We obtain a complete specification that is directly executable, and we discover and fix a number of issues in the pseudocode. These results were facilitated by the already detailed pseudocode of Derecho and made possible by using DistAlgo, a language that allows distributed algorithms to be easily and clearly expressed and directly executed. △ Less

Submitted 19 May, 2023; originally announced May 2023.

Proceedings of the 2nd Workshop on Logic and Practice of Programming (LPOP)

Authors: David S. Warren, Peter Van Roy, Yanhong A. Liu

Abstract: This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop i… ▽ More This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop is to be a bridge between different areas of computer science that use logic as a practical tool. We take advantage of the common language of formal logic to exchange ideas between these different areas. △ Less

Submitted 17 November, 2022; originally announced November 2022.

Programming with rules and everything else, seamlessly

Authors: Yanhong A. Liu, Scott D. Stoller, Yi Tong, Bo Lin, K. Tuncay Tekle

Abstract: Logic rules are powerful for expressing complex reasoning and analysis problems. At the same time, they are inconvenient or impossible to use for many other aspects of applications. Integrating rules in a language with sets and functions, and furthermore with updates to objects, has been a subject of significant study. What's lacking is a language that integrates all constructs seamlessly. This… ▽ More Logic rules are powerful for expressing complex reasoning and analysis problems. At the same time, they are inconvenient or impossible to use for many other aspects of applications. Integrating rules in a language with sets and functions, and furthermore with updates to objects, has been a subject of significant study. What's lacking is a language that integrates all constructs seamlessly. This paper presents a language, Alda, that supports all of rules, sets, functions, updates, and objects as seamlessly integrated built-ins, including concurrent and distributed processes. The key idea is to support predicates as set-valued variables that can be used and updated in any scope, and support queries and inference with both explicit and automatic calls to an inference function. We develop a complete formal semantics for Alda. We design a compilation framework that ensures the declarative semantics of rules, while also being able to exploit available optimizations. We describe a prototype implementation that builds on a powerful extension of Python and employs an efficient logic rule engine. We develop a range of benchmarks and present results of experiments to demonstrate Alda's power for programming and generally good performance. △ Less

Submitted 30 May, 2022; originally announced May 2022.

A Hybrid Science-Guided Machine Learning Approach for Modeling and Optimizing Chemical Processes

Authors: Niket Sharma, Y. A. Liu

Abstract: This study presents a broad perspective of hybrid process modeling and optimization combining the scientific knowledge and data analytics in bioprocessing and chemical engineering with a science-guided machine learning (SGML) approach. We divide the approach into two major categories. The first refers to the case where a data-based ML model compliments and makes the first-principle science-based m… ▽ More This study presents a broad perspective of hybrid process modeling and optimization combining the scientific knowledge and data analytics in bioprocessing and chemical engineering with a science-guided machine learning (SGML) approach. We divide the approach into two major categories. The first refers to the case where a data-based ML model compliments and makes the first-principle science-based model more accurate in prediction, and the second corresponds to the case where scientific knowledge helps make the ML model more scientifically consistent. We present a detailed review of scientific and engineering literature relating to the hybrid SGML approach, and propose a systematic classification of hybrid SGML models. For applying ML to improve science-based models, we present expositions of the sub-categories of direct serial and parallel hybrid modeling and their combinations, inverse modeling, reduced-order modeling, quantifying uncertainty in the process and even discovering governing equations of the process model. For applying scientific principles to improve ML models, we discuss the sub-categories of science-guided design, learning and refinement. For each sub-category, we identify its requirements, advantages and limitations, together with their published and potential areas of applications in bioprocessing and chemical engineering.We also present several examples to illustrate different hybrid SGML methodologies for modeling polymer processes. △ Less

Submitted 24 January, 2022; v1 submitted 2 December, 2021; originally announced December 2021.

Comments: 29 pages 12 figures, 1 table

Proceedings 37th International Conference on Logic Programming (Technical Communications)

Authors: Andrea Formisano, Yanhong Annie Liu, Bart Bogaerts, Alex Brik, Veronica Dahl, Carmine Dodaro, Paul Fodor, Gian Luca Pozzato, Joost Vennekens, Neng-Fa Zhou

Abstract: ICLP is the premier international event for presenting research in logic programming. Contributions to ICLP 2021 were sought in all areas of logic programming, including but not limited to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages issues: Concurrency, Objects, Coordination, Mobility, Higher order, Types, Modes, Assertions, Modules, Meta-… ▽ More ICLP is the premier international event for presenting research in logic programming. Contributions to ICLP 2021 were sought in all areas of logic programming, including but not limited to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages issues: Concurrency, Objects, Coordination, Mobility, Higher order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming techniques. Programming support: Program analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing, Execution visualization. Implementation: Compilation, Virtual machines, Memory management, Parallel and Distributed execution, Constraint handling rules, Tabling, Foreign interfaces, User interfaces. Related Paradigms and Synergies: Inductive and coinductive logic programming, Constraint logic programming, Answer set programming, Interaction with SAT, SMT and CSP solvers, Theorem proving, Argumentation, Probabilistic programming, Machine learning. Applications: Databases, Big data, Data integration and federation, Software engineering, Natural language processing, Web and semantic web, Agents, Artificial intelligence, Computational life sciences, Cyber-security, Robotics, Education. △ Less

Submitted 14 September, 2021; originally announced September 2021.

Journal ref: EPTCS 345, 2021

An Interpretable Algorithm for Uveal Melanoma Subty** from Whole Slide Cytology Images

Authors: Haomin Chen, T. Y. Alvin Liu, Catalina Gomez, Zelia Correa, Mathias Unberath

Abstract: Algorithmic decision support is rapidly becoming a staple of personalized medicine, especially for high-stakes recommendations in which access to certain information can drastically alter the course of treatment, and thus, patient outcome; a prominent example is radiomics for cancer subty**. Because in these scenarios the stakes are high, it is desirable for decision systems to not only provide… ▽ More Algorithmic decision support is rapidly becoming a staple of personalized medicine, especially for high-stakes recommendations in which access to certain information can drastically alter the course of treatment, and thus, patient outcome; a prominent example is radiomics for cancer subty**. Because in these scenarios the stakes are high, it is desirable for decision systems to not only provide recommendations but supply transparent reasoning in support thereof. For learning-based systems, this can be achieved through an interpretable design of the inference pipeline. Herein we describe an automated yet interpretable system for uveal melanoma subty** with digital cytology images from fine needle aspiration biopsies. Our method embeds every automatically segmented cell of a candidate cytology image as a point in a 2D manifold defined by many representative slides, which enables reasoning about the cell-level composition of the tissue sample, paving the way for interpretable subty** of the biopsy. Finally, a rule-based slide-level classification algorithm is trained on the partitions of the circularly distorted 2D manifold. This process results in a simple rule set that is evaluated automatically but highly transparent for human verification. On our in house cytology dataset of 88 uveal melanoma patients, the proposed method achieves an accuracy of 87.5% that compares favorably to all competing approaches, including deep "black box" models. The method comes with a user interface to facilitate interaction with cell-level content, which may offer additional insights for pathological assessment. △ Less

Submitted 13 August, 2021; originally announced August 2021.

Comments: Accepted by ICML 2021 workshop of ILHM

Discrete Math with Programming: A Principled Approach

Authors: Yanhong A. Liu, Matthew Castelllana

Abstract: Discrete mathematics is the foundation of computer science. It focuses on concepts and reasoning methods that are studied using math notations. It has long been argued that discrete math is better taught with programming, which takes concepts and computing methods and turns them into executable programs. What has been lacking is a principled approach that supports all central concepts of discrete… ▽ More Discrete mathematics is the foundation of computer science. It focuses on concepts and reasoning methods that are studied using math notations. It has long been argued that discrete math is better taught with programming, which takes concepts and computing methods and turns them into executable programs. What has been lacking is a principled approach that supports all central concepts of discrete math -- especially predicate logic -- and that directly and precisely connects math notations with executable programs. This paper introduces such an approach. It is based on the use of a powerful language that extends the Python programming language with proper logic quantification ("for all" and "exists some"), as well as declarative set comprehension (also known as set builder) and aggregation (e.g., sum and product). Math and logical statements can be expressed precisely at a high level and be executed directly on a computer, encouraging declarative programming together with algorithmic programming. We describe the approach, detailed examples, experience in using it, and the lessons learned. △ Less

Submitted 27 November, 2020; originally announced November 2020.

Journal ref: Proceedings of the 52nd ACM Technical Symposium on Computer Science Education (SIGCSE 2021), pages 1156-1162, March 2021, ACM Press

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

Authors: Yanhong A. Liu, Scott D. Stoller

Abstract: This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their sa… ▽ More This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties. △ Less

Submitted 23 December, 2020; v1 submitted 21 August, 2020; originally announced August 2020.

Comments: Small fixes to improve property specifications, including improvements not in the RV 2020 final version

Journal ref: RV 2020: Proceedings of the 20th International Conference on Runtime Verification. LNCS 12399. Pages 47-66. Springer

LPOP: Challenges and Advances in Logic and Practice of Programming

Authors: David S. Warren, Yanhong A. Liu

Abstract: This article describes the work presented at the first Logic and Practice of Programming (LPOP) Workshop, which was held in Oxford, UK, on July 18, 2018, in conjunction with the Federated Logic Conference (FLoC) 2018. Its focus is challenges and advances in logic and practice of programming. The workshop was organized around a challenge problem that specifies issues in role-based access control (R… ▽ More This article describes the work presented at the first Logic and Practice of Programming (LPOP) Workshop, which was held in Oxford, UK, on July 18, 2018, in conjunction with the Federated Logic Conference (FLoC) 2018. Its focus is challenges and advances in logic and practice of programming. The workshop was organized around a challenge problem that specifies issues in role-based access control (RBAC), with many participants proposing combined imperative and declarative solutions expressed in the languages of their choice. △ Less

Submitted 15 August, 2020; originally announced August 2020.

Comments: arXiv admin note: substantial text overlap with arXiv:1804.10247 by other authors

Recursive Rules with Aggregation: A Simple Unified Semantics

Authors: Yanhong A. Liu, Scott D. Stoller

Abstract: Complex reasoning problems are most clearly and easily specified using logical rules, but require recursive rules with aggregation such as count and sum for practical applications. Unfortunately, the meaning of such rules has been a significant challenge, leading to many disagreeing semantics. This paper describes a unified semantics for recursive rules with aggregation, extending the unified fo… ▽ More Complex reasoning problems are most clearly and easily specified using logical rules, but require recursive rules with aggregation such as count and sum for practical applications. Unfortunately, the meaning of such rules has been a significant challenge, leading to many disagreeing semantics. This paper describes a unified semantics for recursive rules with aggregation, extending the unified founded semantics and constraint semantics for recursive rules with negation. The key idea is to support simple expression of the different assumptions underlying different semantics, and orthogonally interpret aggregation operations using their simple usual meaning. We present a formal definition of the semantics, prove important properties of the semantics, and compare with prior semantics. In particular, we present an efficient inference over aggregation that gives precise answers to all examples we have studied from the literature. We also apply our semantics to a wide range of challenging examples, and show that our semantics is simple and matches the desired results in all cases. Finally, we describe experiments on the most challenging examples, exhibiting unexpectedly superior performance over well-known systems when they can compute correct answers. △ Less

Submitted 21 September, 2022; v1 submitted 26 July, 2020; originally announced July 2020.

Journal ref: Journal of Logic and Computation, 32(8):1659--1693, December 2022

What's Live? Understanding Distributed Consensus

Authors: Saksham Chand, Yanhong A Liu

Abstract: Distributed consensus algorithms such as Paxos have been studied extensively. They all use the same definition of safety. Liveness is especially important in practice despite well-known theoretical impossibility results. However, many different liveness properties and assumptions have been stated, and there are no systematic comparisons for better understanding of these properties. This paper sy… ▽ More Distributed consensus algorithms such as Paxos have been studied extensively. They all use the same definition of safety. Liveness is especially important in practice despite well-known theoretical impossibility results. However, many different liveness properties and assumptions have been stated, and there are no systematic comparisons for better understanding of these properties. This paper systematically studies and compares different liveness properties stated for over 30 prominent consensus algorithms and variants. We introduce a precise high-level language and formally specify these properties in the language. We then create a hierarchy of liveness properties combining two hierarchies of the assumptions used and a hierarchy of the assertions made, and compare the strengths and weaknesses of algorithms that ensure these properties. Our formal specifications and systematic comparisons led to the discovery of a range of problems in various stated liveness properties, from too weak assumptions for which no liveness assertions can hold, to too strong assumptions making it trivial to achieve the assertions. We also developed TLA+ specifications of these liveness properties, and we use model checking of execution steps to illustrate liveness patterns for Paxos. △ Less

Submitted 21 June, 2021; v1 submitted 14 January, 2020; originally announced January 2020.

Knowledge of Uncertain Worlds: Programming with Logical Constraints

Authors: Yanhong A. Liu, Scott D. Stoller

Abstract: Programming with logic for sophisticated applications must deal with recursion and negation, which together have created significant challenges in logic, leading to many different, conflicting semantics of rules. This paper describes a unified language, DA logic, for design and analysis logic, based on the unifying founded semantics and constraint semantics, that support the power and ease of prog… ▽ More Programming with logic for sophisticated applications must deal with recursion and negation, which together have created significant challenges in logic, leading to many different, conflicting semantics of rules. This paper describes a unified language, DA logic, for design and analysis logic, based on the unifying founded semantics and constraint semantics, that support the power and ease of programming with different intended semantics. The key idea is to provide meta-constraints, supports the use of uncertain information in the form of either undefined values or possible combinations of values or both, and promote the use of knowledge units that can be instantiated by any new predicates, including predicates with additional arguments. △ Less

Submitted 10 December, 2020; v1 submitted 23 October, 2019; originally announced October 2019.

Journal ref: Journal of Logic and Computation, 31(1):193-212, Jan. 2021, Oxford University Press

Extended Magic for Negation: Efficient Demand-Driven Evaluation of Stratified Datalog with Precise Complexity Guarantees

Authors: K. Tuncay Tekle, Yanhong A. Liu

Abstract: Given a set of Datalog rules, facts, and a query, answers to the query can be inferred bottom-up starting from the facts or top-down starting from the query. For efficiency, top-down evaluation is extended with memoization of inferred facts, and bottom-up evaluation is performed after transformations to make rules driven by the demand from the query. Prior work has shown their precise complexity a… ▽ More Given a set of Datalog rules, facts, and a query, answers to the query can be inferred bottom-up starting from the facts or top-down starting from the query. For efficiency, top-down evaluation is extended with memoization of inferred facts, and bottom-up evaluation is performed after transformations to make rules driven by the demand from the query. Prior work has shown their precise complexity analysis and relationships. However, when Datalog is extended with even stratified negation, which has a simple and universally accepted semantics, transformations to make rules demand-driven may result in non-stratified negation, which has had many complex semantics and evaluation methods. This paper presents (1) a simple extension to demand transformation, a transformation to make rules demand-driven for Datalog without negation, to support stratified negation, and (2) a simple extension to an optimal bottom-up evaluation method for Datalog with stratified negation, to handle non-stratified negation in the resulting rules. We show that the method provides precise complexity guarantees. It is also optimal in that only facts needed for top-down evaluation of the query are inferred and each firing of a rule to infer such a fact takes worst-case constant time. We extend the precise relationship between top-down evaluation and demand-driven bottom-up evaluation to Datalog with stratified negation. Finally, we show experimental results for performance, as well as applications to previously challenging examples. △ Less

Submitted 18 September, 2019; originally announced September 2019.

Comments: In Proceedings ICLP 2019, arXiv:1909.07646

ACM Class: D.3.2; H.2.3; D.3.4

Journal ref: EPTCS 306, 2019, pp. 241-254

Algorithm Diversity for Resilient Systems

Authors: Scott D. Stoller, Yanhong A. Liu

Abstract: Diversity can significantly increase the resilience of systems, by reducing the prevalence of shared vulnerabilities and making vulnerabilities harder to exploit. Work on software diversity for security typically creates variants of a program using low-level code transformations. This paper is the first to study algorithm diversity for resilience. We first describe how a method based on high-level… ▽ More Diversity can significantly increase the resilience of systems, by reducing the prevalence of shared vulnerabilities and making vulnerabilities harder to exploit. Work on software diversity for security typically creates variants of a program using low-level code transformations. This paper is the first to study algorithm diversity for resilience. We first describe how a method based on high-level invariants and systematic incrementalization can be used to create algorithm variants. Executing multiple variants in parallel and comparing their outputs provides greater resilience than executing one variant. To prevent different parallel schedules from causing variants' behaviors to diverge, we present a synchronized execution algorithm for DistAlgo, an extension of Python for high-level, precise, executable specifications of distributed algorithms. We propose static and dynamic metrics for measuring diversity. An experimental evaluation of algorithm diversity combined with implementation-level diversity for several sequential algorithms and distributed algorithms shows the benefits of algorithm diversity. △ Less

Submitted 28 April, 2019; originally announced April 2019.

Journal ref: In Proceedings of the 33rd Annual IFIP WG 11.3 Working Conference on Data and Applications Security and Privacy (DBSec 2019), volume 11559 of Lecture Notes in Computer Science. Springer-Verlag, 2019

High-level Cryptographic Abstractions

Authors: Christopher Kane, Bo Lin, Saksham Chand, Scott D. Stoller, Yanhong A. Liu

Abstract: The interfaces exposed by commonly used cryptographic libraries are clumsy, complicated, and assume an understanding of cryptographic algorithms. The challenge is to design high-level abstractions that require minimum knowledge and effort to use while also allowing maximum control when needed. This paper proposes such high-level abstractions consisting of simple cryptographic primitives and full… ▽ More The interfaces exposed by commonly used cryptographic libraries are clumsy, complicated, and assume an understanding of cryptographic algorithms. The challenge is to design high-level abstractions that require minimum knowledge and effort to use while also allowing maximum control when needed. This paper proposes such high-level abstractions consisting of simple cryptographic primitives and full declarative configuration. These abstractions can be implemented on top of any cryptographic library in any language. We have implemented these abstractions in Python, and used them to write a wide variety of well-known security protocols, including Signal, Kerberos, and TLS. We show that programs using our abstractions are much smaller and easier to write than using low-level libraries, where size of security protocols implemented is reduced by about a third on average. We show our implementation incurs a small overhead, less than 5 microseconds for shared key operations and less than 341 microseconds (< 1%) for public key operations. We also show our abstractions are safe against main types of cryptographic misuse reported in the literature. △ Less

Submitted 23 August, 2019; v1 submitted 21 October, 2018; originally announced October 2018.

Journal ref: PLAS 2019: Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security. November 2019. Pages 31-43

Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

Authors: Saksham Chand, Yanhong A. Liu

Abstract: This paper studies specifications and proofs of distributed algorithms when only message history variables are used, using the Basic Paxos and Multi-Paxos algorithms for distributed consensus as precise case studies. We show that not using and maintaining other state variables yields simpler specifications that are more declarative and easier to understand. It also allows easier proofs to be devel… ▽ More This paper studies specifications and proofs of distributed algorithms when only message history variables are used, using the Basic Paxos and Multi-Paxos algorithms for distributed consensus as precise case studies. We show that not using and maintaining other state variables yields simpler specifications that are more declarative and easier to understand. It also allows easier proofs to be developed by needing fewer invariants and facilitating proof derivations. Furthermore, the proofs are mechanically checked more efficiently. We show that specifications in TLA+, Lamport's temporal logic of actions, and proofs in TLAPS, the TLA+ Proof System (TLAPS) are reduced by a quarter or more for single-value Paxos and by about half or more for multi-value Paxos. Overall we need about half as many manually written invariants and proof obligations. Our proof for Basic Paxos takes about 25% less time for TLAPS to check, and our proofs for Multi-Paxos are checked within 1.5 minutes whereas prior proofs fail to be checked by TLAPS. △ Less

Submitted 23 December, 2019; v1 submitted 26 February, 2018; originally announced February 2018.

Logic Programming Applications: What Are the Abstractions and Implementations?

Authors: Yanhong A. Liu

Abstract: This article presents an overview of applications of logic programming, classifying them based on the abstractions and implementations of logic languages that support the applications. The three key abstractions are join, recursion, and constraint. Their essential implementations are for-loops, fixed points, and backtracking, respectively. The corresponding kinds of applications are database queri… ▽ More This article presents an overview of applications of logic programming, classifying them based on the abstractions and implementations of logic languages that support the applications. The three key abstractions are join, recursion, and constraint. Their essential implementations are for-loops, fixed points, and backtracking, respectively. The corresponding kinds of applications are database queries, inductive analysis, and combinatorial search, respectively. We also discuss language extensions and programming paradigms, summarize example application problems by application areas, and touch on example systems that support variants of the abstractions with different implementations. △ Less

Submitted 20 February, 2018; originally announced February 2018.

Journal ref: In M. Kifer and Y.A. Liu, editors, Declarative Logic Programming: Theory, Systems, and Applications, Chapter 10, pages 519-557, ACM and Morgan & Claypool, 2018

AppLP: A Dialogue on Applications of Logic Programming

Authors: David S. Warren, Yanhong A. Liu

Abstract: This document describes the contributions of the 2016 Applications of Logic Programming Workshop (AppLP), which was held on October 17 and associated with the International Conference on Logic Programming (ICLP) in Flushing, New York City. This document describes the contributions of the 2016 Applications of Logic Programming Workshop (AppLP), which was held on October 17 and associated with the International Conference on Logic Programming (ICLP) in Flushing, New York City. △ Less

Submitted 7 April, 2017; originally announced April 2017.

Comments: David S. Warren and Yanhong A. Liu (Editors). 33 pages. Including summaries by Christopher Kane and abstracts or position papers by M. Aref, J. Rosenwald, I. Cervesato, E.S.L. Lam, M. Balduccini, J. Lobo, A. Russo, E. Lupu, N. Leone, F. Ricca, G. Gupta, K. Marple, E. Salazar, Z. Chen, A. Sobhi, S. Srirangapalli, C.R. Ramakrishnan, N. Bjørner, N.P. Lopes, A. Rybalchenko, and P. Tarau

Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms

Authors: Yanhong A. Liu, Saksham Chand, Scott D. Stoller

Abstract: This paper describes the application of a high-level language and method in develo** simpler specifications of more complex variants of the Paxos algorithm for distributed consensus. The specifications are for Multi-Paxos with preemption, replicated state machine, and reconfiguration and optimized with state reduction and failure detection. The language is DistAlgo. The key is to express complex… ▽ More This paper describes the application of a high-level language and method in develo** simpler specifications of more complex variants of the Paxos algorithm for distributed consensus. The specifications are for Multi-Paxos with preemption, replicated state machine, and reconfiguration and optimized with state reduction and failure detection. The language is DistAlgo. The key is to express complex control flows and synchronization conditions precisely at a high level, using nondeterministic waits and message-history queries. We obtain complete executable specifications that are almost completely declarative---updating only a number for the protocol round besides the sets of messages sent and received. We show the following results: 1.English and pseudocode descriptions of distributed algorithms can be captured completely and precisely at a high level, without adding, removing, or reformulating algorithm details to fit lower-level, more abstract, or less direct languages. 2.We created higher-level control flows and synchronization conditions than all previous specifications, and obtained specifications that are much simpler and smaller, even matching or smaller than abstract specifications that omit many algorithm details. 3.The simpler specifications led us to easily discover useless replies, unnecessary delays, and liveness violations (if messages can be lost) in previous published specifications, by just following the simplified algorithm flows. 4.The resulting specifications can be executed directly, and we can express optimizations cleanly, yielding drastic performance improvement over naive execution and facilitating a general method for merging processes. 5.We systematically translated the resulting specifications into TLA+ and developed machine-checked safety proofs, which also allowed us to detect and fix a subtle safety violation in an earlier unpublished specification. △ Less

Submitted 12 August, 2019; v1 submitted 31 March, 2017; originally announced April 2017.

Journal ref: PPDP 2019: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming. October 2019. Article No. 15. Pages 1-15. ACM Press

Precise Complexity Guarantees for Pointer Analysis via Datalog with Extensions

Authors: K. Tuncay Tekle, Yanhong A. Liu

Abstract: Pointer analysis is a fundamental static program analysis for computing the set of objects that an expression can refer to. Decades of research has gone into develo** methods of varying precision and efficiency for pointer analysis for programs that use different language features, but determining precisely how efficient a particular method is has been a challenge in itself. For programs that… ▽ More Pointer analysis is a fundamental static program analysis for computing the set of objects that an expression can refer to. Decades of research has gone into develo** methods of varying precision and efficiency for pointer analysis for programs that use different language features, but determining precisely how efficient a particular method is has been a challenge in itself. For programs that use different language features, we consider methods for pointer analysis using Datalog and extensions to Datalog. When the rules are in Datalog, we present the calculation of precise time complexities from the rules using a new algorithm for decomposing rules for obtaining the best complexities. When extensions such as function symbols and universal quantification are used, we describe algorithms for efficiently implementing the extensions and the complexities of the algorithms. This paper is under consideration for acceptance in TPLP. △ Less

Submitted 8 August, 2016; v1 submitted 4 August, 2016; originally announced August 2016.

Comments: Paper presented at the 32nd International Conference on Logic Programming (ICLP 2016), New York City, USA, 16-21 October 2016, 19 pages, LaTeX

ACM Class: F.3.2; I.2.3; F.2.2

Journal ref: Theory and Practice of Logic Programming, 16(5-6):916-932, Sept. 2016, Cambridge University Press

Founded Semantics and Constraint Semantics of Logic Rules

Authors: Yanhong A. Liu, Scott D. Stoller

Abstract: Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell's paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in… ▽ More Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell's paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in recursion. This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates, rules, and reasoning to be specified explicitly, as simple and precise binary choices. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program. △ Less

Submitted 26 March, 2020; v1 submitted 20 June, 2016; originally announced June 2016.

Journal ref: Journal of Logic and Computation, 30(8):1609-1668, Dec. 2020, Oxford University Press

Formal Verification of Multi-Paxos for Distributed Consensus

Authors: Saksham Chand, Yanhong A. Liu, Scott D. Stoller

Abstract: Paxos is an important algorithm for a set of distributed processes to agree on a single value or a sequence of values, for which it is called Basic Paxos or Multi-Paxos, respectively. Consensus is critical when distributed services are replicated for fault-tolerance, because non-faulty replicas must agree on the state of the system or the sequence of operations that have been performed. Unfortunat… ▽ More Paxos is an important algorithm for a set of distributed processes to agree on a single value or a sequence of values, for which it is called Basic Paxos or Multi-Paxos, respectively. Consensus is critical when distributed services are replicated for fault-tolerance, because non-faulty replicas must agree on the state of the system or the sequence of operations that have been performed. Unfortunately, consensus algorithms including Multi-Paxos in particular are well-known to be difficult to understand, and their accurate specifications and correctness proofs remain challenging, despite extensive studies ever since Lamport introduced Paxos. This article describes formal specification and verification of Lamport's Multi-Paxos algorithm for distributed consensus. The specification is written in TLA+, Lamport's Temporal Logic of Actions. The proof is written and automatically checked using TLAPS, the TLA+ Proof System. The proof is for the safety property of the algorithm. Building on Lamport, Merz, and Doligez's specification and proof for Basic Paxos, we aim to facilitate the understanding of Multi-Paxos and its proof by minimizing the difference from those for Basic Paxos, and to demonstrate a general way of proving other variants of Paxos and other sophisticated distributed algorithms. We also discuss our general strategies and results for proving complex invariants using invariance lemmas and increments, for proving properties about sets and tuples to help the proof check succeed in significantly reduced time, and for overall proof improvement leading to considerably reduced proof size. △ Less

Submitted 11 November, 2019; v1 submitted 4 June, 2016; originally announced June 2016.

Journal ref: FM 2016: Proceedings of the 21st International Symposium on Formal Methods. LNCS 9995. Pages 119-136. Springer,

Demand-Driven Incremental Object Queries

Authors: Yanhong A. Liu, Jon Brandvein, Scott D. Stoller, Bo Lin

Abstract: Object queries are essential in information seeking and decision making in vast areas of applications. However, a query may involve complex conditions on objects and sets, which can be arbitrarily nested and aliased. The objects and sets involved as well as the demand---the given parameter values of interest---can change arbitrarily. How to implement object queries efficiently under all possible u… ▽ More Object queries are essential in information seeking and decision making in vast areas of applications. However, a query may involve complex conditions on objects and sets, which can be arbitrarily nested and aliased. The objects and sets involved as well as the demand---the given parameter values of interest---can change arbitrarily. How to implement object queries efficiently under all possible updates, and furthermore to provide complexity guarantees? This paper describes an automatic method. The method allows powerful queries to be written completely declaratively. It transforms demand as well as all objects and sets into relations. Most importantly, it defines invariants for not only the query results, but also all auxiliary values about the objects and sets involved, including those for propagating demand, and incrementally maintains all of them. Implementation and experiments with problems from a variety of application areas, including distributed algorithms and probabilistic queries, confirm the analyzed complexities, trade-offs, and significant improvements over prior work. △ Less

Submitted 15 July, 2016; v1 submitted 14 November, 2015; originally announced November 2015.

Journal ref: PPDP 2016: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, September 2016, Pages 228-241. ACM Press

From Clarity to Efficiency for Distributed Algorithms

Authors: Yanhong A. Liu, Scott D. Stoller, Bo Lin

Abstract: This article describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would b… ▽ More This article describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly. We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms. △ Less

Submitted 11 March, 2017; v1 submitted 29 December, 2014; originally announced December 2014.

Journal ref: ACM Transactions on Programming Languages and Systems (TOPLAS), 39(3), pages 12:1-12:41, July 2017, ACM Press