Levent Erkök

Formal Verification Engineer at Apple.
Beaverton, OR.

Basics

• CV
• Linked-in
• E-mail: erkokl at gmail.com

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

Papers

• 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)