4 Search Results for "Kaufman, Arie"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.43
Inductive Predicate Synthesis Modulo Programs

Authors: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analysis tools operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analysis tool to the solver. For example, an analysis tool for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis. Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks - such as parameterized model checking - to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a real-world application to smart-contract verification.
Cite as

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 43:1-43:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wesley_et_al:LIPIcs.ECOOP.2024.43,
  author =	{Wesley, Scott and Christakis, Maria and Navas, Jorge A. and Trefler, Richard and W\"{u}stholz, Valentin and Gurfinkel, Arie},
  title =	{{Inductive Predicate Synthesis Modulo Programs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{43:1--43:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan 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.2024.43},
  URN =		{urn:nbn:de:0030-drops-208926},
  doi =		{10.4230/LIPIcs.ECOOP.2024.43},
  annote =	{Keywords: Software Verification, Invariant Synthesis, Model-Checking}
}
Document
DOI: 10.4230/DagRep.1.6.1
Scientific Visualization (Dagstuhl Seminar 11231)

Authors: Min Chen, Hans Hagen, Charles D. Hansen, and Arie Kaufman

Published in: Dagstuhl Reports, Volume 1, Issue 6 (2011)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 11231 ``Scientific Visualization''.
Cite as

Min Chen, Hans Hagen, Charles D. Hansen, and Arie Kaufman. Scientific Visualization (Dagstuhl Seminar 11231). In Dagstuhl Reports, Volume 1, Issue 6, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{chen_et_al:DagRep.1.6.1,
  author =	{Chen, Min and Hagen, Hans and Hansen, Charles D. and Kaufman, Arie},
  title =	{{Scientific Visualization (Dagstuhl Seminar 11231)}},
  pages =	{1--23},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{6},
  editor =	{Chen, Min and Hagen, Hans and Hansen, Charles D. and Kaufman, Arie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.6.1},
  URN =		{urn:nbn:de:0030-drops-32574},
  doi =		{10.4230/DagRep.1.6.1},
  annote =	{Keywords: Scientific Visualization, Biomedical Visualization, Integrated Multifield Visualization, Uncertainty Visualization, Scalable Visualization}
}
Document
DOI: 10.4230/DagSemProc.09251.1
09251 Abstracts Collection – Scientific Visualization

Authors: David S. Ebert, Eduard Gröller, Hans Hagen, and Arie Kaufman

Published in: Dagstuhl Seminar Proceedings, Volume 9251, Scientific Visualization (2010)

Abstract
From 06-14-2009 to 06-19-2009, the Dagstuhl Seminar 09251 ``Scientific Visualization '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, over 50 international participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general.
Cite as

David S. Ebert, Eduard Gröller, Hans Hagen, and Arie Kaufman. 09251 Abstracts Collection – Scientific Visualization. In Scientific Visualization. Dagstuhl Seminar Proceedings, Volume 9251, pp. 1-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ebert_et_al:DagSemProc.09251.1,
  author =	{Ebert, David S. and Gr\"{o}ller, Eduard and Hagen, Hans and Kaufman, Arie},
  title =	{{09251 Abstracts Collection – Scientific Visualization}},
  booktitle =	{Scientific Visualization},
  pages =	{1--36},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9251},
  editor =	{David S. Ebert and Eduard Gr\"{o}ller and Hans Hagen and Arie Kaufman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09251.1},
  URN =		{urn:nbn:de:0030-drops-27436},
  doi =		{10.4230/DagSemProc.09251.1},
  annote =	{Keywords: Scientific visualization, Data analysis, Data modeling, Segmentation, Knowledge extraction, Ubiquitous visualization, Categorical visualization, Intelligent/automatic visualization, Point-based/mesh-free visualization}
}
Document
DOI: 10.4230/DFU.SciViz.2010.246
Visual Simulation of Flow

Authors: Arie Kaufman and Ye Zhao

Published in: Dagstuhl Follow-Ups, Volume 1, Scientific Visualization: Advanced Concepts (2010)

Abstract
We have adopted a numerical method from computational fluid dynamics, the Lattice Boltzmann Method (LBM), for real-time simulation and visualization of flow and amorphous phenomena, such as clouds, smoke, fire, haze, dust, radioactive plumes, and air-borne biological or chemical agents. Unlike other approaches, LBM discretizes the micro-physics of local interactions and can handle very complex boundary conditions, such as deep urban canyons, curved walls, indoors, and dynamic boundaries of moving objects. Due to its discrete nature, LBM lends itself to multi-resolution approaches, and its computational pattern, which is similar to cellular automata, is easily parallelizable. We have accelerated LBM on commodity graphics processing units (GPUs), achieving real-time or even accelerated real-time on a single GPU or on a GPU cluster. We have implemented a 3D urban navigation system and applied it in New York City with real-time live sensor data. In addition to a pivotal application in simulation of airborne contaminants in urban environments, this approach will enable the development of other superior prediction simulation capabilities, computer graphics and games, and a novel technology for computational science and engineering.
Cite as

Arie Kaufman and Ye Zhao. Visual Simulation of Flow. In Scientific Visualization: Advanced Concepts. Dagstuhl Follow-Ups, Volume 1, pp. 246-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InCollection{kaufman_et_al:DFU.SciViz.2010.246,
  author =	{Kaufman, Arie and Zhao, Ye},
  title =	{{Visual Simulation of Flow}},
  booktitle =	{Scientific Visualization: Advanced Concepts},
  pages =	{246--258},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-19-4},
  ISSN =	{1868-8977},
  year =	{2010},
  volume =	{1},
  editor =	{Hagen, Hans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DFU.SciViz.2010.246},
  URN =		{urn:nbn:de:0030-drops-27080},
  doi =		{10.4230/DFU.SciViz.2010.246},
  annote =	{Keywords: Lattice Boltzmann Method, Amorphous phenomena, GPU Acceleration, Computational Fluid Dynamics, Urban Security}
}
  • Refine by Author
  • 3 Kaufman, Arie
  • 2 Hagen, Hans
  • 1 Chen, Min
  • 1 Christakis, Maria
  • 1 Ebert, David S.
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Software verification

  • Refine by Keyword
  • 1 Amorphous phenomena
  • 1 Biomedical Visualization
  • 1 Categorical visualization
  • 1 Computational Fluid Dynamics
  • 1 Data analysis
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2010
  • 1 2011
  • 1 2024

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact