Formal Verification Engineer at Apple.
Software (on GitHub)
- SBV: SMT Based Verification in Haskell
- SBVPlugin: GHC Core-plugin for SBV
- HArduino: Control your Arduino from Haskell
- Linear: Solve systems of Linear Equations
- FloatingHex: Hexadecimal Floats for Haskell
- CrackNum: Decode/encode IEEE-754 Floating point numbers
- ConjugateGradient: Sparse matrix linear equation solver
- ISMT: Yices as an Isabelle theorem prover tactic
Warren E. Ferguson, Jesse Bingham, Levent Erkök, John R. Harrison, Joe Leslie-Hurd. Digit serial methods with aplications to division and square root. IEEE Transactions on Computers, 67(3):449–456, March 2018. (bib) (Arxiv version with proofs)
Levent Erkök, Noura Amjadi. Counting ECC failures using Formal Methods to substantiate RAS claims. Intel Design and Test Technology Conference, DTTC’17, 2017. [not electronically available] (bib)
Levent Erkök, Flemming Andersen, John Matthews. Formal Verification of SECDED-ECC RTL using functional programs as golden models.
Intel Design and Test Technology Conference, DTTC’12, 2012. [not electronically available] (bib)
Iavor Diatchi, Lee Pike, Levent Erkök. Practical Considerations in Control-Flow Integrity Monitoring.
In Second International Workshop on Security Testing Workshop, SECTEST’11, Berlin, Germany, March 2011, IEEE. (bib)
Levent Erkök, Magnus Carlsson, Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol.
In Formal Methods in Computer Aided Design Conference, FMCAD’09, Austin, TX, November 2009, IEEE. (slides) (bib)
Levent Erkök, John Matthews. High assurance programming in Cryptol.
In CSIIRW’09: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research, Oak Ridge, TN, April 2009, ACM. (bib)
Levent Erkök, John Matthews. Pragmatic Equivalence and Safety Checking in Cryptol.
In Programming Languages meets Program Verification Workshop, PLPV’09. Savannah, Georgia, USA. January, 2009. (slides) (bib)
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews. Imperative Functional Programming with Isabelle/HOL.
Proc. of 2008 Theorem Proving and Higher Order Logics Conference, TPHOLS’08. Montreal, Canada. August, 2008. (bib)
Levent Erkök, John Matthews. Using Yices as an automated solver in Isabelle/HOL.
Automated Formal Methods’08, Princeton, New Jersey, USA. July, 2008. (slides) (bib)
Rebekah Leslie, Levent Erkök, Flemming Andersen. Formalizing Information Flow in a Haskell Hypervisor.
Microkernels and Embedded Systems Workshop, MIKES’07. Sydney, Australia. January, 2007. (bib)
Levent Erkök. Application of formal methods in factory automation to reduce configuration-induced misprocessing risks.
International Sematech APC/AEC Symposium XVI, Poster Session, September 2004. (bib)
Levent Erkök. Formal verification of controller transactions using Computation Tree Logic.
Intel Design and Test Technology Conference, DTTC’04, August 2004. [not electronically available] (bib)
Levent Erkök. Value Recursion in Monadic Computations.
PhD Dissertation, Oregon Graduate Institute School of Science Engineering, OHSU. October 2002. (bib) (slides) (errata)
Levent Erkök, John Launchbury. A Recursive do for Haskell.
Proc. of 2002 ACM SIGPLAN Workshop on Haskell, Haskell’02 (Pittsburgh, PA, USA, 3 Oct. 2002), pp. 29-37, ACM Press, 2002. (bib)
Levent Erkök, John Launchbury, Andrew Moran. Semantics of Value Recursion for Monadic Input/Output.
Theoretical Informatics and Applications, 36(2), pp. 155-180, 2002. (bib)
Levent Erkök, John Launchbury, Andrew Moran. Semantics of fixIO.
Workshop on Fixed points in Computer Science Workshop, FICS’01. Firenze, Italy. September, 2001. (bib)
Levent Erkök, John Launchbury. Recursive Monadic Bindings.
Proc. of 5th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP’00 (Montréal, Canada, 18–21 Sept. 2000), pp. 174-185, ACM Press, 2000. (bib)
Levent Erkök, John Launchbury. A Recursive do for Haskell: Design and Implementation.
Technical Report CSE-00-14, Oregon Graduate Institute Of Science and Technology, August 2000. (bib)
Levent Erkök, John Launchbury. Recursive Monadic Bindings: Technical Development and Details.
Technical Report CSE-00-11, Oregon Graduate Institute Of Science and Technology, June 2000. (bib)
Levent Erkök. A partial evaluator and post-optimizer for a flow chart language.
M.Sc. Thesis, Middle East Technical University, Ankara, Turkey. July 1997. (bib)
Osman Burçhan Bayazıt, Levent Erkök, Okan Uludağ, Fatoş Yarman Vural. Gray Level Texture Generation by Binary Markov Random Field Model with Morphological Operations.
Technical Report 95-10, Middle East Technical University Computer Engineering Department, July 1995. (bib)