Skip to content

Commit

Permalink
First version of l11 (application highlights)
Browse files Browse the repository at this point in the history
  • Loading branch information
domschrei committed Jun 27, 2024
1 parent cabc394 commit 259ac7b
Show file tree
Hide file tree
Showing 21 changed files with 817 additions and 0 deletions.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/3d-miter-visualization.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/algorithm-engineering.pdf
Binary file not shown.
Binary file added slides/figures/l11/bmc.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/circuits-aig.pdf
Binary file not shown.
Binary file added slides/figures/l11/circuits-miter.pdf
Binary file not shown.
Binary file added slides/figures/l11/circuits.pdf
Binary file not shown.
Binary file added slides/figures/l11/decisiontree-improvement.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/decisiontree-smaller.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/decisiontree.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/jml.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/mapf-large.pdf
Binary file not shown.
Binary file added slides/figures/l11/mapf-small.pdf
Binary file not shown.
Binary file added slides/figures/l11/mapf.pdf
Binary file not shown.
Binary file added slides/figures/l11/train-scheduling.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added slides/figures/l11/transition-system-bmc.pdf
Binary file not shown.
Binary file added slides/figures/l11/transition-system.pdf
Binary file not shown.
Binary file added slides/figures/l11/wordcloud3-crop.pdf
Binary file not shown.
Binary file added slides/l11-applications.pdf
Binary file not shown.
607 changes: 607 additions & 0 deletions slides/l11-applications.tex

Large diffs are not rendered by default.

210 changes: 210 additions & 0 deletions slides/references.bib
Original file line number Diff line number Diff line change
Expand Up @@ -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}
}

0 comments on commit 259ac7b

Please sign in to comment.