From a8bb7736e2e86963bd5761cc05079447abeeaba6 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Tue, 23 Jun 2026 15:26:01 +0200 Subject: using official template + fixing language errors --- biblio.bib | 229 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 229 insertions(+) create mode 100644 biblio.bib (limited to 'biblio.bib') diff --git a/biblio.bib b/biblio.bib new file mode 100644 index 0000000..e3a73fc --- /dev/null +++ b/biblio.bib @@ -0,0 +1,229 @@ +@inproceedings{lafont1990interactionnets, + author = {Lafont, Yves}, + title = {Interaction nets}, + year = {1989}, + isbn = {0897913434}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/96709.96718}, + doi = {10.1145/96709.96718}, + abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.}, + booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + pages = {95–108}, + numpages = {14}, + location = {San Francisco, California, USA}, + series = {POPL '90} +} +@inproceedings{demoura2008z3, + author="de Moura, Leonardo + and Bj{\o}rner, Nikolaj", + editor="Ramakrishnan, C. R. + and Rehof, Jakob", + title="Z3: An Efficient SMT Solver", + booktitle="Tools and Algorithms for the Construction and Analysis of Systems", + year="2008", + publisher="Springer Berlin Heidelberg", + address="Berlin, Heidelberg", + pages="337--340", + abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", + isbn="978-3-540-78800-3" +} +@misc{kumar2019equivalentapproximatetransformationsdeep, + title={Equivalent and Approximate Transformations of Deep Neural Networks}, + author={Abhinav Kumar and Thiago Serra and Srikumar Ramalingam}, + year={2019}, + eprint={1905.11428}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/1905.11428}, +} +@article{JMLR:v24:21-0579, + author = {Fenglei Fan and Rongjie Lai and Ge Wang}, + title = {Quasi-Equivalence between Width and Depth of Neural Networks}, + journal = {Journal of Machine Learning Research}, + year = {2023}, + volume = {24}, + number = {183}, + pages = {1--22}, + url = {http://jmlr.org/papers/v24/21-0579.html} +} +@misc{kaulen20256thinternationalverificationneural, + title={The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results}, + author={Konstantin Kaulen and Tobias Ladner and Stanley Bak and Christopher Brix and Hai Duong and Thomas Flinkow and Taylor T. Johnson and Lukas Koller and Edoardo Manino and ThanhVu H Nguyen and Haoze Wu}, + year={2025}, + eprint={2512.19007}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/2512.19007}, +} +@article{fisher1936iris, + author = {FISHER, R. A.}, + title = {THE USE OF MULTIPLE MEASUREMENTS IN TAXONOMIC PROBLEMS}, + journal = {Annals of Eugenics}, + volume = {7}, + number = {2}, + pages = {179-188}, + doi = {https://doi.org/10.1111/j.1469-1809.1936.tb02137.x}, + url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1469-1809.1936.tb02137.x}, + eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1469-1809.1936.tb02137.x}, + abstract = {The articles published by the Annals of Eugenics (1925–1954) have been made available online as an historical archive intended for scholarly use. The work of eugenicists was often pervaded by prejudice against racial, ethnic and disabled groups. The online publication of this material for scholarly research purposes is not an endorsement of those views nor a promotion of eugenics in any way.}, + year = {1936} +} +@article{lecun2010mnist, + title={MNIST handwritten digit database}, + author={LeCun, Yann and Cortes, Corinna and Burges, CJ}, + journal={ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist}, + volume={2}, + year={2010} +} +@InProceedings{eleftheriadis2022equivalence, + author="Eleftheriadis, Charis + and Kekatos, Nikolaos + and Katsaros, Panagiotis + and Tripakis, Stavros", + editor="Bogomolov, Sergiy + and Parker, David", + title="On Neural Network Equivalence Checking Using SMT Solvers", + booktitle="Formal Modeling and Analysis of Timed Systems", + year="2022", + publisher="Springer International Publishing", + address="Cham", + pages="237--257", + abstract="Two pretrained neural networks are deemed (approximately) equivalent if they yield similar outputs for the same inputs. Equivalence checking of neural networks is of great importance, due to its utility in replacing learning-enabled components with (approximately) equivalent ones, when there is need to fulfill additional requirements or to address security threats, as is the case when using knowledge distillation, adversarial training, etc. In this paper, we present a method to solve various strict and approximate equivalence checking problems for neural networks, by reducing them to SMT satisfiability checking problems. This work explores the utility and limitations of the neural network equivalence checking framework, and proposes avenues for future research and improvements toward more scalable and practically applicable solutions. We present experimental results, for diverse types of neural network models (classifiers and regression networks) and equivalence criteria, towards a general and application-independent equivalence checking approach.", + isbn="978-3-031-15839-1" +} + +@article{rosenblatt1958perceptron, + added-at = {2017-07-19T15:29:59.000+0200}, + author = {Rosenblatt, F.}, + biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez}, + citeulike-article-id = {13697582}, + citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519}, + doi = {10.1037/h0042519}, + interhash = {dc0cef9dc06033a04f525efdcde7a660}, + intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9}, + issn = {0033-295X}, + journal = {Psychological Review}, + keywords = {imported}, + number = 6, + pages = {386--408}, + posted-at = {2016-05-02 20:23:36}, + priority = {2}, + timestamp = {2017-07-19T15:31:02.000+0200}, + title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}}, + url = {http://dx.doi.org/10.1037/h0042519}, + volume = 65, + year = 1958 +} +@article{rumelhart1986learning, + title={Learning representations by back-propagating errors}, + author={Rumelhart, David E and Hinton, Geoffrey E and Williams, Ronald J}, + journal={Nature}, + volume={323}, + number={6088}, + pages={533--536}, + year={1986}, + publisher={Nature Publishing Group} +} + +@inproceedings{katz2017reluplex, + title={Reluplex: An efficient SMT solver for verifying deep neural networks}, + author={Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={97--117}, + year={2017}, + organization={Springer} +} + +@inproceedings{katz2019marabou, + title={The Marabou framework for verification and analysis of deep neural networks}, + author={Katz, Guy and Huang, Derek A and Ibeling, Duligur and Julian, Kyle and Burns, Ryan and Sadigh, Dorsa and Barrett, Clark and Dill, David L and Kochenderfer, Mykel J}, + booktitle={International Conference on Computer Aided Verification}, + pages={443--452}, + year={2019}, + organization={Springer} +} + +@article{barrett2016smtlib, + title={The SMT-LIB standard: Version 2.6}, + author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare}, + journal={Department of Computer Science, The University of Iowa, Tech. Rep}, + year={2016} +} +@misc{wang2018efficientformalsafetyanalysis, + title={Efficient Formal Safety Analysis of Neural Networks}, + author={Shiqi Wang and Kexin Pei and Justin Whitehouse and Junfeng Yang and Suman Jana}, + year={2018}, + eprint={1809.08098}, + archivePrefix={arXiv}, + primaryClass={cs.LG}, + url={https://arxiv.org/abs/1809.08098}, +} +@incollection{dantzig1947simplex, + abstract = {In 1947, George Dantzig created a simplex algorithm to solve linear programs for planning and decision-making in large-scale enterprises. The algorithm's success led to a vast array of specializations and generalizations that have dominated practical operations research for half a century}, + added-at = {2010-02-26T23:23:28.000+0100}, + address = {Piscataway, NJ, USA}, + author = {Nash, John C.}, + biburl = {https://www.bibsonomy.org/bibtex/2b85e2108e8f7cc402a52577323035ad9/ytyoun}, + booktitle = {Computing in Science and Engg.}, + doi = {10.1109/5992.814654}, + interhash = {5fb3b9e4a0e81f7811c917b86d1097cb}, + intrahash = {b85e2108e8f7cc402a52577323035ad9}, + issn = {1521-9615}, + keywords = {algorithm magazine matrix simplex top.ten.algorithms}, + number = 1, + pages = {29--31}, + publisher = {IEEE Educational Activities Department}, + timestamp = {2015-12-13T09:44:24.000+0100}, + title = {The (Dantzig) Simplex Method for Linear Programming}, + volume = 2, + year = 2000 +} +@article{zhang2018efficient, + title={Efficient Neural Network Robustness Certification with General Activation Functions}, + author={Zhang, Huan and Weng, Tsui-Wei and Chen, Pin-Yu and Hsieh, Cho-Jui and Daniel, Luca}, + journal={Advances in Neural Information Processing Systems}, + volume={31}, + pages={4939--4948}, + year={2018}, + url={https://arxiv.org/pdf/1811.00866.pdf} +} +@article{xu2020automatic, + title={Automatic perturbation analysis for scalable certified robustness and beyond}, + author={Xu, Kaidi and Shi, Zhouxing and Zhang, Huan and Wang, Yihan and Chang, Kai-Wei and Huang, Minlie and Kailkhura, Bhavya and Lin, Xue and Hsieh, Cho-Jui}, + journal={Advances in Neural Information Processing Systems}, + volume={33}, + year={2020} +} +@inproceedings{xu2021fast, + title={{Fast and Complete}: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers}, + author={Kaidi Xu and Huan Zhang and Shiqi Wang and Yihan Wang and Suman Jana and Xue Lin and Cho-Jui Hsieh}, + booktitle={International Conference on Learning Representations}, + year={2021}, + url={https://openreview.net/forum?id=nVZtXBI6LNn} +} +@article{wang2021beta, + title={{Beta-CROWN}: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification}, + author={Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, + journal={Advances in Neural Information Processing Systems}, + volume={34}, + year={2021} +} +@inproceedings{shi2024genbab, + title={Neural Network Verification with Branch-and-Bound for General Nonlinearities}, + author={Shi, Zhouxing and Jin, Qirui and Kolter, Zico and Jana, Suman and Hsieh, Cho-Jui and Zhang, Huan}, + booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, + year={2025} +} +@article{zhang2022general, + title={General Cutting Planes for Bound-Propagation-Based Neural Network Verification}, + author={Zhang, Huan and Wang, Shiqi and Xu, Kaidi and Li, Linyi and Li, Bo and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico}, + journal={Advances in Neural Information Processing Systems}, + year={2022} +} +@inproceedings{zhou2024scalable, + title={Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes}, + author={Zhou, Duo and Brix, Christopher and Hanasusanto, Grani A and Zhang, Huan}, + booktitle={The Thirty-eighth Annual Conference on Neural Information Processing Systems}, + year={2024} +} -- cgit v1.2.3