Personal Details
| Work address | Imperial College London | |
| Department of Computing | ||
| 180 Queen's Gate | ||
| London SW7 2BZ | ||
| United Kingdom | ||
| kws at doc dot ic dot ac dot uk | ||
| susanto at computer dot org |
Education
| Philosophy Doctor in Computing Science, University of Glasgow, United Kingdom | ||
| Master in Artificial Intelligence (cum laude), Katholieke Universiteit Leuven, Belgium | ||
| Bachelor of Science in Mathematics and Statistics, The Open University, United Kingdom | ||
| Sarjana Teknik in Electronics Engineering, Universitas Kristen Satya Wacana, Indonesia |
Professional Trainings and Certifications
| 2007 | Certificate Cisco Certified Network Associate | |
| Cisco Systems Inc. | ||
| 2005 | Certificate Panduit Network Infrastructure Essentials | |
| Cisco Net-Academy | ||
| 2004 | Certificate Specman Advanced Training Course | |
| Verisity UK | ||
| 1998, | Cadence Training Courses | |
| 1999 | Cadence, Scotland | |
| Tools: Verilog XL, LeapFrog, BuildGates, Pearl, Composer, Silicon Ensemble, | ||
| Design Planner, IC Craftsman, TDD, BBD | ||
| 1996 | Certificate Knowledge Based Techniques for Automated Analog Designs | |
| Faculty of Electronics Engineering | ||
| Katholieke Universiteit Leuven, Belgium | ||
| 1994 | Certificate Chemical Cutter Operator | |
| Halliburton, USA | ||
| 1994 | Certificate Field Logging Engineer | |
| Halliburton, USA | ||
| 1993 | Certificate Basic Accounting | |
| Faculty of Economics | ||
| Universitas kristen Satya Wacana, Indonesia |
Professional Experiences
| 2007 - 2011 | Post Doctoral Research Associate | |
| Department of Computing, Imperial College London, UK | ||
| 2005 - 2007 | Post Doctoral Research Associate | |
| Computer Laboratory, University of Cambridge, UK | ||
| 2004 - 2005 | Associate Consultant | |
| Verilab Ltd. UK | ||
| 1998 - 2003 | Teaching Assistant | |
| Dept. of Computing Science, University of Glasgow, UK | ||
| 2000 - 2001 | Senior CAD Engineer (Doctoral Internship) | |
| Strategic CAD Labs., INTEL Corp. USA | ||
| 1997 - 2001 | Research Assistant | |
| Dept. of Computing Science, University of Glasgow, UK | ||
| 1996 - 1997 | Research and Development Engineer (Research Fellow) | |
| Interuniversitair MicroElectronica Centreum (IMEC) | ||
| Katholieke Universiteit Leuven, Belgium | ||
| 1993 - 1995 | Field Logging Engineer | |
| Halliburton Energy Services, Indonesia | ||
| 1990 - 1992 | Teaching Assistant | |
| Dept. of Electronics Engineering, Universitas Kristen Satya Wacana, Indonesia |
Project Summaries
hArtes (Imperial College London)
| + | Analysed and formalised the correctness of program transformations |
| + | Developing a methodology for automatic proof script generations for code optimisations |
| + | Developed a methodology to integrate Metis ATP into Isabelle ITP |
| + | Developed characterization procedures for First Order and Higher Order problems |
| + | Developed proof reconstruction procedures for Metis proof steps in Isabelle |
| + | Re-developed the CONMAX RTL and test-bench in System-Verilog. |
| + | Improved the RTL with parameterization for the number of masters and slaves generation. |
| + | Achieved significant RTL code improvements, code reduction by 85%. |
| + | Re-developed the APB GPIO RTL and Test-bench in System-Verilog. |
| + | Developed assertion properties to monitor and validate the data-path events. |
| + | In comparison to verilog style coding, the RTL code size is reduced to 50%. |
| + | Developed an automatic test-cases generator in systemC to specifically targeted |
| the SDHC (Secured Digital Host Controller) module of the Multi-media Card System. | |
| + | Developed a set of constraints for various memory card system and set of instructions in SCV. |
| + | Developed test-bench for UART 16550 in Specman/e (eRM compliance). |
| + | Developed eRM components for the test-bench; Serial data eVC and Wishbone eVC. |
| + | Developed directed validation test-cases targeted for functional validation of |
| Giga-bit Ethernet MAC chip in Specman/e. | |
| + | Key tasks includes developing test strategies to validate registers files, |
| reset and interrupt sequences, and module connectivity and functionality. |
| + | Developed a Formal Verification Platform methodology for the verification of System |
| on Chip design using an integrated heterogeneous formal verification environment | |
| + | Developed a methodology to verify the correctness of a hardware/software system. |
| + | Developed an integrated formal verification environment which combined |
| the power of ACL2, HOL, and SMV. | |
| + | Developed a parser from SMV to HOL in ML Lex and Yacc. |
| + | Developed an executable ARM7 formal model in LISP. |
| + | Validate AMBA bus protocol (Verilog) and obtained a set of AMBA AHB properties. |
| + | Developed an SoC platform based on ARM7 and AMBA bus protocol and produced the |
| requirement properties for additional modules which will satisfy the top level requirements. |
| + | Developed a full coverage verification code for the FADD data-path functionality. |
| + | Rejuvenating formal verification code for Pentium IV Control and Retirement Unit. |
| + | Developed a methodology to validate the functional correctness of on the fly algorithm |
| to reconfigure circuits at execution time. | |
| + | Developed semantics of net-list language in PVS. |
| + | Developed a formal model of an FPGA cell and structure in PVS. |
| + | Developed a synthesize-able processor core based on PIC16C5X specification in VHDL. |
| + | Developed a methodology to validate the processor core. |
| + | The validation is based on case splitting techniques on the state transition diagram. |
| + | Developed a parser (symbolic analyser) in C that analyzed VHDL code and transformed it |
| to symbolic models (COSMOS). | |
| + | Developed a methodology to validate an embedded system. |
| + | Developed a compiler that generate binary code from assembly code for the MCS-51 |
| micro-controller family. | |
| + | Developed a simulator for the MCS-51 micro-controller family. |
| + | Designed and produced an instrument to measure the rotation of an A.C. motor. |
Publications
| + | Kong Woei Susanto and Wayne Luk |
| Automating Formal Verification of Customized Soft Processors | |
| International Conference on Field Programmable Technology 2011 (accepted). | |
| + | Kong Woei Susanto, Tim Todman, Jose Gabriel Coutinho, and Wayne Luk |
| Design Validation by Symbolic Simulation and Equivalence Checking: | |
| A Case Study in Memory Optimization for Image Manipulation. | |
| International Conference in Software Seminars (SOFSEM'09), January 2009, Myln-Czech, LNCS 5404. | |
| + | Kong Woei Susanto, Wayne Luk, Jose Gabriel Coutinho, and Tim Todman |
| Validating Design Optimisation. | |
| Tools and Techniques for Verification of System Infrastructure (TTVSI'08), March 2008, London, pp. 36. | |
| + | Larry Paulson and Kong Woei Susanto |
| Source-Level Proof Reconstruction for Interactive Theorem Proving. | |
| International Conference of Theorem Proving and Higer Order Logics (TPHOLs'07), September 2007, Kaiserlautern-Germany, LNCS 4732, pp. 232-245. | |
| + | Kong Woei Susanto and Tom Melham |
| AMBA-ARM7 Formal Verification Platform. | |
| International Conference of Formal Engineering Methods (ICFEM'03), November 2003, Singapore, LNCS 2885, pp. 48-67. | |
| + | Kong Woei Susanto |
| An Integrated Formal Approach for System on Chip. | |
| International Workshop in IP Based Design 2002, October 2002, Grenoble-France, pp. 119-123. | |
| + | K.W. Susanto and Tom Melham |
| Formally Analysed Dynamic Synthesis of Hardware. | |
| Journal of Supercomputing, vol. 19, no. 1, May 2001, pp. 7-22. | |
| + | K.W. Susanto and Tom Melham |
| Formally Analysed Dynamic Synthesis of Hardware. | |
| 11th International Conference, TPHOLs'98, Canberra, September - October 1998, | |
| Supplementary Proceedings, Australian National University, 1998, Canberra-Australia, pp. 105-117. | |
| + | N. McKay, T. Melham, K. W. Susanto, and S. Singh |
| Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation. | |
| IEEE Symposium on FPGAs for Custom Computing Machines: April 1998, Napa Valley, California, pp. 308-309. | |
| + | PhD Thesis: A Verification Platform for System on Chip. |
| Supervisors: Prof. Tom Melham and Dr. Simon Gay | |
| + | Master Dissertation: Symbolic Verification for Embedded Hardware/Software Systems. |
| Supervisor: Prof.Dr.Ir. Luc Claesen | |
| + | S.T. Dissertation: Assembler and Simulator for Microcontroller Family of MCS-51 and |
| its Application as Tool for Designing an Instrument that Measure the Rotation of an A.C. motor. | |
| Supervisors: Dr. C.E. Prince Jr., Ir. M. Prasetyo O. |
Awards
| 1998-2002 | Overseas Research Scholarship (ORS), UK. | |
| 1997-2002 | Postgraduate Research Studentship, University of Glasgow, UK. | |
| 1996-1997 | Research Fellowship, Katholieke Universiteit Leuven, Belgium |
Professional Memberships
| + | Institute of Electrical and Electronics Engineers, member, since 1991. |
| + | Association for Computing Machinery, Professional member, since 1997. |
| + | Badminton Scotland, Assistant Coach, since 2010. |
Interests and Past activities
| + | Voluntary healthy and balanced diet cooking teacher (keeping well for greater govan project, 2006). |
| + | GKI Salatiga Choir Leader (1990-1992). |
| + | University Senate member, International Relation division (1990-1991). |
| + | Selected for East Asia Student Encounter Program. an exchange student program with Kwansei Gakuin University-Japan (1989, 1990). |
| + | Voluntary Physics and Mathematics teacher in an orphanage house (1988-1991). |
| + | Faculty Student Council member (1988-1989). |
| + | Sports: Badminton, Tennis, Table Tennis, Swimming. |
| + | Hobbies: Contract Bridge (Participate in National Contract Bridge Competition), Jigsaw Puzzles (9000+). |