I studied computer science with mathematics as a minor subject at the RWTH Aachen since 2004. From July 2010 to 2015, I worked as a research assistant at Chair for Logic and Verification.
| Address: |
Technische Universität München Institut für Informatik Boltzmannstr. 3 85748 Garching Deutschland |
|---|
Currently I am working on formalizing some aspects of graph theory in the Isabelle theorem prover. This involves verifying certifying algorithms in the LEDA graph library and Random Graphs.
Publications
Journal Articles
-
A Graph Library for Isabelle.
Lars Noschinski
Mathematics in Computer Science, March 2015, Volume 9, Issue 1, pp 23-39
local copy. The final publication is available at http://link.springer.com. -
Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs.
Lars Noschinski, Fabian Emmes, Jürgen Giesl
Journal of Automated Reasoning, June 2013, Volume 51, Issue 1, pp 27-56
The final publication is available at http://link.springer.com.
Conference Papers
- Experience Report: The Next 1100 Haskell Programmers.
Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, Dmitriy Traytel
Proceedings of the ACM SIGPLAN Symposium on Haskell (Haskell 2014). ACM BibTeX
local copy. The final publication is available at dx.doi.org/10.1145/2633357.2633359. - Verification of Certifying Computations through AutoCorres and Simpl.
Lars Noschinski, Christine Rizkallah, and Kurt Mehlhorn
Proceedings of the NFM 2014. Springer BibTeX
local copy. The final publication is available at http://link.springer.com. The source of the proof is available here. -
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem.
Lars Noschinski
Proceedings of the ITP 2012. Springer BibTeX
local copy. The final publication is available at http://link.springer.com. The source of the proof is available in the AFP. -
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems.
Lars Noschinski, Fabian Emmes and Jürgen Giesl.
Proceedings of the CADE 2011. Springer. BibTeX
local copy. The final publication is available at http://link.springer.com. An extended version appeared as Technical Report AIB-2011-03, RWTH Aachen, Germany.
Workshop Papers
-
Pattern-based Subterm Selection in Isabelle.
Christoph Traut and Lars Noschinski.
Isabelle Workshop 2014. BibTeX
local copy. -
Towards Structured Proofs for Program Verification (Ongoing Work).
Lars Noschinski.
Isabelle Workshop 2014 BibTeX
local copy.
Drafts
-
Formalizing Graph Theory and Planarity Certificates.
Ph.D. thesis. Fakultät für Informatik, Technische Universität München. Submitted November 2015. BibTex
Diploma thesis
-
Automated Complexity Analysis of Term Rewrite Systems.
Diploma thesis. Fakultät für Mathematik, Informatik und Naturwissenschaften, RWTH Aachen. March 2010. BibTex