Levent Erkök
Intel Corporation
2501 NW 229th Ave
Hillsboro, OR 97124
Email: erkokl at gmail.com
Curriculum Vitae
Software (on GitHub)
 SBV: SMT Based Verification in Haskell
 SBVPlugin: GHC Coreplugin for SBV
 HArduino: Control your Arduino from Haskell
 Linear: Solve systems of Linear Equations
 CrackNum: Decode/encode IEEE754 Floating point numbers
 ConjugateGradient: Sparse matrix linear equation solver
 ISMT: Yices as an Isabelle theorem prover tactic
Papers

Levent Erkök, Flemming Andersen, John Matthews
Formal Verification of SECDEDECC 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 ControlFlow 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 Coverification 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 configurationinduced 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. 2937, 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. 155180, 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. 174185, ACM Press, 2000. (bib) 
Levent Erkök, John Launchbury
A Recursive do for Haskell: Design and Implementation
Technical Report CSE0014, Oregon Graduate Institute Of Science and Technology, August 2000. (bib) 
Levent Erkök, John Launchbury
Recursive Monadic Bindings: Technical Development and Details
Technical Report CSE0011, Oregon Graduate Institute Of Science and Technology, June 2000. (bib) 
Levent Erkök
A partial evaluator and postoptimizer 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 9510, Middle East Technical University Computer Engineering Department, July 1995. (bib)