First version of l11 (application highlights)

Author: domschrei

slides/figures/l11/3d-large-miter-visualization.jpg

@@ -669,3 +669,213 @@ @inproceedings{Inprocessing:2012
 url="http://dx.doi.org/10.1007/978-3-642-31365-3_28"
 }
  
+@article{clarke2001bounded,
+	title={Bounded model checking using satisfiability solving},
+	author={Clarke, Edmund and Biere, Armin and Raimi, Richard and Zhu, Yunshan},
+	journal={Formal methods in system design},
+	volume={19},
+	pages={7--34},
+	year={2001},
+	publisher={Springer}
+}
+
+@inproceedings{falke2013bounded,
+	title={The bounded model checker {LLBMC}},
+	author={Falke, Stephan and Merz, Florian and Sinz, Carsten},
+	booktitle={2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE)},
+	pages={706--709},
+	year={2013},
+	organization={IEEE}
+}
+
+@InProceedings{vizel2015boolean,
+	author    = {Yakir Vizel and Georg Weissenbacher and Sharad Malik},
+	title     = {Boolean Satisfiability Solvers and Their Applications in Model Checking},
+	booktitle = {Proc. {IEEE}},
+	year      = {2015},
+	volume    = {103},
+	number    = {11},
+	pages     = {2021--2035},
+	doi       = {10.1109/JPROC.2015.2455034},
+	bibsource = {dblp computer science bibliography, https://dblp.org},
+	biburl    = {https://dblp.org/rec/journals/pieee/VizelWM15.bib},
+	timestamp = {Fri, 02 Oct 2020 14:42:28 +0200},
+}
+
+@inproceedings{beckert2020modular,
+	title={Modular verification of {JML} contracts using bounded model checking},
+	author={Beckert, Bernhard and Kirsten, Michael and Klamroth, Jonas and Ulbrich, Mattias},
+	booktitle={Int.\ Symposium on Leveraging Applications of Formal Methods (ISoLA)},
+	pages={60--80},
+	year={2020},
+	organization={Springer}
+}
+
+@article{koch2021card,
+	title={Card-based cryptography meets formal verification},
+	author={Koch, Alexander and Schrempp, Michael and Kirsten, Michael},
+	journal={New Generation Computing},
+	volume={39},
+	number={1},
+	pages={115--158},
+	year={2021},
+	publisher={Springer}
+}
+
+@inproceedings{kuehlmann2004dynamic,
+	title={Dynamic transition relation simplification for bounded property checking},
+	author={Kuehlmann, Andreas},
+	booktitle={IEEE/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004.},
+	pages={50--57},
+	year={2004},
+	organization={IEEE}
+}
+
+@InProceedings{biere2022gimsatul,
+	author    = {Biere, Armin and Fleury, Mathias},
+	title     = {Gimsatul, {IsaSAT}, {Kissat} Entering the {SAT} Competition 2022},
+	booktitle = {SAT Competition},
+	year      = {2022},
+	pages     = {10--11},
+}
+
+@InProceedings{gao2023kissat,
+	author    = {Gao, Yu},
+	title     = {{Kissat\_MAB\_prop} in {SAT} Competition 2023},
+	booktitle = {SAT Competition},
+	year      = {2023},
+	pages     = {16},
+}
+
+@InProceedings{marques2000boolean,
+	author    = {Marques-Silva, Jo{\~a}o P. and Sakallah, Karem A.},
+	title     = {Boolean satisfiability in electronic design automation},
+	booktitle = {Proc. DAC},
+	year      = {2000},
+	pages     = {675--680},
+	doi       = {10.1145/337292.337611},
+}
+
+@Article{surynek2022migrating,
+	author  = {Surynek, Pavel and Stern, Roni and Boyarski, Eli and Felner, Ariel},
+	title   = {Migrating Techniques from Search-Based Multi-Agent Path Finding Solvers to {SAT}-Based Approach},
+	journal = {JAIR},
+	year    = {2022},
+	volume  = {73},
+	pages   = {553--618},
+	doi     = {10.1613/jair.1.13318},
+}
+
+@misc{weaver2015equivalence,
+	author={Weaver, Sean},
+	title={Equivalence Checking},
+	howpublished={\url{https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/Equivalence_Checking_11_30_08.pdf}},
+	year={2015}
+}
+
+@inproceedings{narodytska2018learning,
+	title={Learning optimal decision trees with {SAT}},
+	author={Narodytska, Nina and Ignatiev, Alexey and Pereira, Filipe and Marques-Silva, Joao},
+	booktitle={International Joint Conference on Artificial Intelligence 2018},
+	pages={1362--1368},
+	year={2018},
+	organization={Association for the Advancement of Artificial Intelligence (AAAI)}
+}
+
+@inproceedings{schidler2021sat,
+	title={{SAT}-based decision tree learning for large data sets},
+	author={Schidler, Andr{\'e} and Szeider, Stefan},
+	booktitle={AAAI conference on artificial intelligence},
+	volume={35},
+	number={5},
+	pages={3904--3912},
+	year={2021}
+}
+
+@InProceedings{froleyks2019pasar,
+	author    = {Froleyks, Nils and Balyo, Tom{\'a}{\v{s}} and Schreiber, Dominik},
+	title     = {{PASAR}---Planning as Satisfiability with Abstraction Refinement},
+	booktitle = {Proc. SoCS},
+	year      = {2019},
+	volume    = {10},
+	number    = {1},
+	pages     = {70--78},
+	url       = {https://ojs.aaai.org/index.php/SOCS/article/download/18504/18295},
+}
+
+@InProceedings{soos09extending,
+	author       = {Mate Soos and Karsten Nohl and Claude Castelluccia},
+	title        = {Extending {SAT} Solvers to Cryptographic Problems},
+	booktitle    = {Theory and Applications of Satisfiability Testing (SAT)},
+	year         = {2009},
+	organization = {Springer},
+	pages        = {244--257},
+	doi          = {10.1007/978-3-642-02777-2_24},
+}
+
+@article{lafitte2014applications,
+	title={Applications of {SAT} solvers in cryptanalysis: finding weak keys and preimages},
+	author={Lafitte, Fr{\'e}d{\'e}ric and Nakahara Jr, Jorge and Van Heule, Dirk},
+	journal={Journal on Satisfiability, Boolean Modeling and Computation},
+	volume={9},
+	number={1},
+	pages={1--25},
+	year={2014},
+	publisher={IOS Press}
+}
+
+@inproceedings{mironov2006applications,
+	title={Applications of {SAT} solvers to cryptanalysis of hash functions},
+	author={Mironov, Ilya and Zhang, Lintao},
+	booktitle={Theory and Applications of Satisfiability Testing-SAT 2006: 9th International Conference, Seattle, WA, USA, August 12-15, 2006. Proceedings 9},
+	pages={102--115},
+	year={2006},
+	organization={Springer}
+}
+
+@inproceedings{xin2019improved,
+	title={Improved cryptanalysis on SipHash},
+	author={Xin, Wenqian and Liu, Yunwen and Sun, Bing and Li, Chao},
+	booktitle={International Conference on Cryptology and Network Security},
+	pages={61--79},
+	year={2019},
+	organization={Springer}
+}
+
+@InProceedings{manthey2023testing,
+	author    = {Manthey, Norbert},
+	title     = {Testing the {ASCON} Hash Function},
+	booktitle = {SAT Competition},
+	year      = {2023},
+	pages     = {63},
+}
+
+@inproceedings{dobraunig2015cryptanalysis,
+	title={Cryptanalysis of ascon},
+	author={Dobraunig, Christoph and Eichlseder, Maria and Mendel, Florian and Schl{\"a}ffer, Martin},
+	booktitle={Topics in Cryptology---CT-RSA 2015: The Cryptographer's Track at the RSA Conference 2015, San Francisco, CA, USA, April 20-24, 2015. Proceedings},
+	pages={371--387},
+	year={2015},
+	organization={Springer}
+}
+
+@InProceedings{weaver2020constructing,
+	author    = {Weaver, Sean and Heule, Marijn J. H.},
+	title     = {Constructing minimal perfect hash functions using {SAT} technology},
+	booktitle = {AAAI Conference on Artificial Intelligence},
+	year      = {2020},
+	volume    = {34},
+	number    = {02},
+	pages     = {1668--1675},
+	doi       = {10.1609/aaai.v34i02.5529},
+}
+
+@article{lemos2024iterative,
+	title={Iterative Train Scheduling under Disruption with Maximum Satisfiability},
+	author={Lemos, Alexandre and Gouveia, Filipe and Monteiro, Pedro T and Lynce, Ines},
+	journal={Journal of Artificial Intelligence Research},
+	volume={79},
+	pages={1047--1090},
+	year={2024}
+}
+