7 Search Results for "Seshia, Sanjit A."

Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2023.38
Building Code Transpilers for Domain-Specific Languages Using Program Synthesis (Experience Paper)

Authors: Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, and Alvin Cheung

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Domain-specific languages (DSLs) are prevalent across many application domains. Such languages let developers easily express computations using high-level abstractions that result in performant implementations. To leverage DSLs, however, application developers need to master the DSL’s syntax and manually rewrite existing code. Compilers can aid in this effort, but part of building a compiler requires transpiling code from the source code to the target DSL. Such transpilation is typically done via pattern-matching rules on the source code. Sadly, developing such rules is often a painstaking and error-prone process. In this paper, we describe our experience in using program synthesis to build code transpilers. To do so, we developed MetaLift, a new framework for building transpilers that transform general-purpose code into DSLs using program synthesis. To use MetaLift, transpiler developers first define the target DSL’s semantics using MetaLift’s specification language, and specify the search space for each input code fragment to be transpiled using MetaLift’s API. MetaLift then leverages program synthesizers and theorem provers to automatically find transpilations expressed in the target DSL that is provably semantic equivalent to the input code. We have used MetaLift to build three DSL transpilers targeting different programming models and application domains. Our results show that the MetaLift-based compilers can translate many benchmarks used in prior work created by specialized implementations, but can be built using orders-of-magnitude fewer lines of code as compared to prior work.
Cite as

Sahil Bhatia, Sumer Kohli, Sanjit A. Seshia, and Alvin Cheung. Building Code Transpilers for Domain-Specific Languages Using Program Synthesis (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 38:1-38:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bhatia_et_al:LIPIcs.ECOOP.2023.38,
  author =	{Bhatia, Sahil and Kohli, Sumer and Seshia, Sanjit A. and Cheung, Alvin},
  title =	{{Building Code Transpilers for Domain-Specific Languages Using Program Synthesis}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{38:1--38:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.38},
  URN =		{urn:nbn:de:0030-drops-182316},
  doi =		{10.4230/LIPIcs.ECOOP.2023.38},
  annote =	{Keywords: Program Synthesis, Code Transpilation, DSLs, Verification}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{04:1--04:34},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/LITES.8.2.7
Real-Time Verification for Distributed Cyber-Physical Systems

Authors: Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent transportation, where autonomous vehicles communicate and cooperate with each other via a high-speed communication network. Such systems require an ability to identify maneuvers in real-time that cause dangerous circumstances and ensure the implementation always meets safety-critical requirements. In this paper, we propose a real-time decentralized reachability approach for safety verification of a distributed multi-agent CPS with the underlying assumption that all agents are time-synchronized with a low degree of error. In the proposed approach, each agent periodically computes its local reachable set and exchanges this reachable set with the other agents with the goal of verifying the system safety. Our method, implemented in Java, takes advantages of the timing information and the reachable set information that are available in the exchanged messages to reason about the safety of the whole system in a decentralized manner. Any particular agent can also perform local safety verification tasks based on their local clocks by analyzing the messages it receives. We applied the proposed method to verify, in real-time, the safety properties of a group of quadcopters performing a distributed search mission.
Cite as

Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. Real-Time Verification for Distributed Cyber-Physical Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 07:1-07:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{tran_et_al:LITES.8.2.7,
  author =	{Tran, Hoang-Dung and Nguyen, Luan Viet and Musau, Patrick and Xiang, Weiming and Johnson, Taylor T.},
  title =	{{Real-Time Verification for Distributed Cyber-Physical Systems}},
  booktitle =	{LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems},
  pages =	{07:1--07:19},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Tran, Hoang-Dung and Nguyen, Luan Viet and Musau, Patrick and Xiang, Weiming and Johnson, Taylor T.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.7},
  doi =		{10.4230/LITES.8.2.7},
  annote =	{Keywords: Verification, Reachability Analysis, Distributed Cyber-Physical Systems}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2020.5
Algorithmic Improvisation for Dependable Intelligent Autonomy (Invited Talk)

Authors: Sanjit A. Seshia

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
Algorithmic Improvisation, also called control improvisation or controlled improvisation, is a new framework for automatically synthesizing systems with specified random but controllable behavior. In this talk, I will present the theory of algorithmic improvisation and show how it can be used in a wide variety of applications where randomness can provide variety, robustness, or unpredictability while guaranteeing safety or other properties. Applications demonstrated to date include robotic surveillance, software fuzz testing, music improvisation, human modeling, generating test cases for simulating cyber-physical systems, and generation of synthetic data sets to train and test machine learning algorithms. In this talk, I will particularly focus on applications to the design of intelligent autonomous systems, presenting work on randomized planning for robotics and a domain-specific probabilistic programming language for the design and analysis of learning-based autonomous systems.
Cite as

Sanjit A. Seshia. Algorithmic Improvisation for Dependable Intelligent Autonomy (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 5:1-5:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{seshia:LIPIcs.FSTTCS.2020.5,
  author =	{Seshia, Sanjit A.},
  title =	{{Algorithmic Improvisation for Dependable Intelligent Autonomy}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.5},
  URN =		{urn:nbn:de:0030-drops-132465},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.5},
  annote =	{Keywords: Formal methods, synthesis, verification, randomized algorithms, formal specification, testing, machine learning, synthetic data generation, planning}
}
Document
DOI: 10.4230/DagRep.7.8.55
Machine Learning and Formal Methods (Dagstuhl Seminar 17351)

Authors: Sanjit A. Seshia, Xianjin (Jerry) Zhu, Andreas Krause, and Susmit Jha

Published in: Dagstuhl Reports, Volume 7, Issue 8 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17351 "Machine Learning and Formal Methods". The seminar brought together practitioners and reseachers in machine learning and related areas (such as robotics) with those working in formal methods and related areas (such as programming languages and control theory). The meeting highlighted the connections between the two disciplines, and created new links between the two research communities.
Cite as

Sanjit A. Seshia, Xianjin (Jerry) Zhu, Andreas Krause, and Susmit Jha. Machine Learning and Formal Methods (Dagstuhl Seminar 17351). In Dagstuhl Reports, Volume 7, Issue 8, pp. 55-73, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{seshia_et_al:DagRep.7.8.55,
  author =	{Seshia, Sanjit A. and Zhu, Xianjin (Jerry) and Krause, Andreas and Jha, Susmit},
  title =	{{Machine Learning and Formal Methods (Dagstuhl Seminar 17351)}},
  pages =	{55--73},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{8},
  editor =	{Seshia, Sanjit A. and Zhu, Xianjin (Jerry) and Krause, Andreas and Jha, Susmit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.8.55},
  URN =		{urn:nbn:de:0030-drops-84302},
  doi =		{10.4230/DagRep.7.8.55},
  annote =	{Keywords: Formal Methods, Machine Learning}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.463
Control Improvisation

Authors: Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We formalize and analyze a new automata-theoretic problem termed control improvisation. Given an automaton, the problem is to produce an improviser, a probabilistic algorithm that randomly generates words in its language, subject to two additional constraints: the satisfaction of an admissibility predicate, and the exhibition of a specified amount of randomness. Control improvisation has multiple applications, including, for example, generating musical improvisations that satisfy rhythmic and melodic constraints, where admissibility is determined by some bounded divergence from a reference melody. We analyze the complexity of the control improvisation problem, giving cases where it is efficiently solvable and cases where it is #P-hard or undecidable. We also show how symbolic techniques based on Boolean satisfiability (SAT) solvers can be used to approximately solve some of the intractable cases.
Cite as

Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel. Control Improvisation. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 463-474, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fremont_et_al:LIPIcs.FSTTCS.2015.463,
  author =	{Fremont, Daniel J. and Donz\'{e}, Alexandre and Seshia, Sanjit A. and Wessel, David},
  title =	{{Control Improvisation}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{463--474},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.463},
  URN =		{urn:nbn:de:0030-drops-56596},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.463},
  annote =	{Keywords: finite automata, random sampling, Boolean satisfiability, testing, computational music, control theory}
}
Document
DOI: 10.4230/DagRep.4.8.89
Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351)

Authors: Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, and Aditya Thakur

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14351 "Decision Procedures and Abstract Interpretation". The seminar brought together practitioners and reseachers in abstract interpretation and decision procedures. The meeting highlighted the connections between the two disciplines, and created new links between the two research communities. Joint activities were also conducted with the participants of Dagstuhl Seminar 14352 "Next Generation Static Software Analysis Tools", which was held concurrently.
Cite as

Daniel Kroening, Thomas W. Reps, Sanjit A. Seshia, and Aditya Thakur. Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351). In Dagstuhl Reports, Volume 4, Issue 8, pp. 89-106, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{kroening_et_al:DagRep.4.8.89,
  author =	{Kroening, Daniel and Reps, Thomas W. and Seshia, Sanjit A. and Thakur, Aditya},
  title =	{{Decision Procedures and Abstract Interpretation (Dagstuhl Seminar 14351)}},
  pages =	{89--106},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Kroening, Daniel and Reps, Thomas W. and Seshia, Sanjit A. and Thakur, Aditya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.8.89},
  URN =		{urn:nbn:de:0030-drops-48007},
  doi =		{10.4230/DagRep.4.8.89},
  annote =	{Keywords: Program analysis, Abstract interpretation, Abstract domain, Fixed-point finding, Satisfiability checking, Satisfiability modulo theories, Decision pro}
}
  • Refine by Author
  • 5 Seshia, Sanjit A.
  • 1 Bhatia, Sahil
  • 1 Cheung, Alvin
  • 1 Donzé, Alexandre
  • 1 Fremont, Daniel J.
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Artificial intelligence
  • 1 Computing methodologies → Distributed computing methodologies
  • 1 Computing methodologies → Distributed programming languages
  • 1 Computing methodologies → Machine learning
  • 1 Computing methodologies → Model verification and validation
  • Show More...

  • Refine by Keyword
  • 2 Verification
  • 2 testing
  • 1 Abstract domain
  • 1 Abstract interpretation
  • 1 Active Objects
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2022
  • 1 2014
  • 1 2015
  • 1 2018
  • 1 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact