Samin Ishtiaq
PRINCIPAL RSDE
.
Samin Ishtiaq is an RSDE in the Programming Principles and Tools group at Microsoft Research Cambridge. He currently works on the SLAyer (Separation Logic-based memory safety for C programs), TERMINATOR (program termination) and BMA (analysis of gene regulatory networks) projects.
Samin has an MEng from Imperial and a PhD in dependent type theory from Queen Mary; he was an RA on the original Verified Bytecode project (1999-2000). Samin worked at ARM (2000-2008) where he did CPU modeling and verification to help tape-out the Cortex A8, Cortex M3 and SC300 processors, and the AMBA bus protocol checker. Samin joined MSR in April 2008.
The Ishtiaq-O'Hearn POPL'01 paper won the Most Influential POPL Paper Award for 2011.
Downloads
Publications
- Benque D., Bourton S., Cockerton C., Cook B., Fisher J., Ishtiaq S., Piterman N., Taylor A., and Vardi M., Bio Model Analyzer: Visual Tool for Modeling and Analysis of Biological Networks, in Computer Aided Verification (CAV) 2012. LNCS 7358, pp. 686–692 , Springer Verlag, July 2012
- Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic--based Analyses, in Proceedings of the 24th International Conference on Computer Aided Verification (CAV), Springer, July 2012
- Josh Berdine, Arlen Cox, Samin Ishtiaq, and Christoph M. Wintersteiger, Diagnosing Abstraction Failure for Separation Logic--based Analyses, no. MSR-TR-2012-44, April 2012
- Josh Berdine, Byron Cook, and Samin Ishtiaq, SLAyer: Memory Safety for Systems-level Code, in CAV, 2011
- Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli, The Semantics of Power and ARM Multiprocessor Machine Code, in Workshop on Declarative Aspects of Multicore Programming, 2009
- Nathan Chong and Samin Ishtiaq, Reasoning about the ARM weakly consistent memory model, in ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, 2008
- Nathan Chong and Samin Ishtiaq, Functional Programming for Hardware Definition, Verification and Modelling, in Hardware Design and Functional Languages , 2007
- Samin Ishtiaq, Verification of the AMBA Protocol, in IEEE 7th International Workshop on Microprocessor Test & Verification, 2006
- Samin Ishtiaq and Peter O'Hearn, BI as an Assertion Language for Mutable Data Structures, in POPL, 2001
- Cristiano Calcagno, Samin Ishtiaq, and Peter O'Hearn, Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic, in PPDP, 2000
- S Ishtiaq and DJ Pym, Kripke Resource Models of a Dependently-typed, Bunched {lambda}-calculus, in Computer Science Logic, 1999
- S Ishtiaq and DJ Pym, A Relevant Analysis of Natural Deduction, in Journal of Logic and Computation, 1998
