diff --git a/thys/Combinable_Wands/document/root.bib b/thys/Combinable_Wands/document/root.bib --- a/thys/Combinable_Wands/document/root.bib +++ b/thys/Combinable_Wands/document/root.bib @@ -1,100 +1,111 @@ @inproceedings{Dockins2009, author = {Dockins, Robert and Hobor, Aquinas and Appel, Andrew W.}, pages = {161--177}, title = {{A Fresh Look at Separation Algebras and Share Accounting}}, booktitle = {Asian Symposium on Programming Languages and Systems (APLAS)}, editor = {Zhenjiang Hu}, year = {2009} } @inproceedings{Calcagno2007, author = {Calcagno, Cristiano and O'Hearn, Peter W. and Yang, Hongseok}, pages = {366--375}, title = {{Local Action and Abstract Separation Logic}}, booktitle = {Logic in Computer Science (LICS)}, year = {2007} } @inproceedings{SchwerhoffSummers15, author = {M. Schwerhoff and A. J. Summers}, title = {{Lightweight Support for Magic Wands in an Automatic Verifier}}, booktitle = {European Conference on Object-Oriented Programming (ECOOP)}, pages = {614--638}, series = {LIPIcs}, year = {2015}, volume = {37}, editor = {J. T. Boyland}, publisher = {Schloss Dagstuhl}, } @inproceedings{Dardinier22, - author = {Dardinier, Thibault and Parthasarathy, Gaurav and Weeks, No\'e and M\"uller, Peter and Summers, Alexander J.}, - title = {{Sound Automation of Magic Wands}}, - booktitle = {Computer Aided Verification (CAV)}, - year = {2022}, - note = {To appear} +author="Dardinier, Thibault +and Parthasarathy, Gaurav +and Weeks, No{\'e} +and M{\"u}ller, Peter +and Summers, Alexander J.", +editor="Shoham, Sharon +and Vizel, Yakir", +title="Sound Automation of Magic Wands", +booktitle="Computer Aided Verification", +year="2022", +publisher="Springer International Publishing", +address="Cham", +pages="130--151", +isbn="978-3-031-13188-2" } + + @inproceedings{Reynolds02a, author = {J. C. Reynolds}, title = {{Separation Logic: A Logic for Shared Mutable Data Structures}}, booktitle = {Logic in Computer Science (LICS)}, Publisher = {IEEE}, pages = {55--74}, year = {2002} } @inproceedings{Boyland03, author="Boyland, John", editor="Cousot, Radhia", title="Checking Interference with Fractional Permissions", booktitle="Static Analysis (SAS)", year="2003", pages="55--72", } @article{Boyland10, author = {John Tang Boyland}, title = {Semantics of fractional permissions with nesting}, journal = {Transactions on Programming Languages and Systems (TOPLAS)}, volume = {32}, number = {6}, pages = {22:1--22:33}, year = {2010}, doi = {10.1145/1749608.1749611}, biburl = {https://dblp.org/rec/journals/toplas/Boyland10.bib} } @inproceedings{JacobsPiessens11, author = {Bart Jacobs and Frank Piessens}, title = {Expressive modular fine-grained concurrency specification}, booktitle = {Principles of Programming Languages (POPL)}, pages = {271--282}, year = {2011}, doi = {10.1145/1926385.1926417}, biburl = {https://dblp.org/rec/conf/popl/JacobsP11.bib} } @inproceedings{LeHobor18, author="Le, Xuan-Bach and Hobor, Aquinas", editor="Ahmed, Amal", title="Logical Reasoning for Disjoint Permissions", booktitle="European Symposium on Programming (ESOP)", year="2018" } @inproceedings{Brotherston20, author="Brotherston, James and Costa, Diana and Hobor, Aquinas and Wickerson, John", editor="Lahiri, Shuvendu K. and Wang, Chao", title="Reasoning over Permissions Regions in Concurrent Separation Logic", booktitle="Computer Aided Verification (CAV)", year="2020" } diff --git a/thys/Package_logic/document/root.bib b/thys/Package_logic/document/root.bib --- a/thys/Package_logic/document/root.bib +++ b/thys/Package_logic/document/root.bib @@ -1,47 +1,56 @@ @inproceedings{Dockins2009, author = {Dockins, Robert and Hobor, Aquinas and Appel, Andrew W.}, pages = {161--177}, title = {{A Fresh Look at Separation Algebras and Share Accounting}}, booktitle = {Asian Symposium on Programming Languages and Systems (APLAS)}, editor = {Zhenjiang Hu}, year = {2009} } @inproceedings{Calcagno2007, author = {Calcagno, Cristiano and O'Hearn, Peter W. and Yang, Hongseok}, pages = {366--375}, title = {{Local Action and Abstract Separation Logic}}, booktitle = {Logic in Computer Science (LICS)}, year = {2007} } @inproceedings{SchwerhoffSummers15, author = {M. Schwerhoff and A. J. Summers}, title = {{Lightweight Support for Magic Wands in an Automatic Verifier}}, booktitle = {European Conference on Object-Oriented Programming (ECOOP)}, pages = {614--638}, series = {LIPIcs}, year = {2015}, volume = {37}, editor = {J. T. Boyland}, publisher = {Schloss Dagstuhl}, } -@inproceedings{Dardinier22, - author = {Dardinier, Thibault and Parthasarathy, Gaurav and Weeks, No\'e and M\"uller, Peter and Summers, Alexander J.}, - title = {{Sound Automation of Magic Wands}}, - booktitle = {Computer Aided Verification (CAV)}, - year = {2022}, - note = {To appear} +@InProceedings{Dardinier22, +author="Dardinier, Thibault +and Parthasarathy, Gaurav +and Weeks, No{\'e} +and M{\"u}ller, Peter +and Summers, Alexander J.", +editor="Shoham, Sharon +and Vizel, Yakir", +title="Sound Automation of Magic Wands", +booktitle="Computer Aided Verification", +year="2022", +publisher="Springer International Publishing", +address="Cham", +pages="130--151", +isbn="978-3-031-13188-2" } @inproceedings{Reynolds02a, author = {J. C. Reynolds}, title = {{Separation Logic: A Logic for Shared Mutable Data Structures}}, booktitle = {Logic in Computer Science (LICS)}, Publisher = {IEEE}, pages = {55--74}, year = {2002} } diff --git a/thys/Package_logic/document/root.tex b/thys/Package_logic/document/root.tex --- a/thys/Package_logic/document/root.tex +++ b/thys/Package_logic/document/root.tex @@ -1,78 +1,76 @@ \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} %for \, \, \, \, \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \, \, \, \, %\ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \newcommand{\wand}{\ensuremath{\mathbin{-\!\!*}}} \newcommand{\cwand}{\ensuremath{\mathbin{-\!\!*}_c}} \newcommand{\twand}{\ensuremath{\mathbin{-\!\!*}_{\mathcal{T}}}} \begin{document} \title{Formalization of a Framework for the Sound Automation of Magic Wands} \author{Thibault Dardinier} \maketitle \begin{abstract} -The magic wand $\wand$ (also called separating implication) is a separation logic~\cite{Reynolds02a} connective % I find it a bit tricky that we talk about the connective and a formula built from it as if these were the same thing +The magic wand $\wand$ (also called separating implication) is a separation logic~\cite{Reynolds02a} connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A \emph{footprint} of a magic wand formula $A \wand B$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called \emph{packaging} a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or are unsound. In this entry, we formally define a framework for the sound automation of magic wands, described in a paper at CAV~2022~\cite{Dardinier22}, and prove that it is sound and complete. This framework, called the \emph{package logic}, precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. -%Moreover, we define a novel, restricted definition of wands, called \emph{combinable wands}, and prove that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. -%Finally, we instantiate the package logic to show our framework can also be used with combinable wands. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: