coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Jobs for undergrads / MS students with proof chops

From: William Simmons <wsimmons.math AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Jobs for undergrads / MS students with proof chops
Date: Wed, 25 Jan 2023 22:00:36 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wsimmons.math AT gmail.com; spf=Pass smtp.mailfrom=wsimmons.math AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f181.google.com
Ironport-data: A9a23:XCe1bqMmDnMxdibvrR1/k8FynXyQoLVcMsEvi/4bfWQNrUp20jMOy 2EdCD+EO6vbZjD2ctB3a4nipBhXsJXUztQyGXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/jgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQDNNwJcaDpOsPra8k035ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXbInXT/fNfKHszftZIwP5oPEUSt qwhfWVlghCr34pawZq+Q+how90/dYzlZdNG/H5nyj7dALAtRpWrr6fiv4cJmmdtwJkQRbCHN 5NxhTlHNHwsZzVQIVYSDZU4h6Gtj2X/WzJdoVOR46Ew5gA/ySQhgeSzaIGLJbRmQ+1crluDv 0WYol+lPRQWMtiOlAuB8FOz07qncSTTAdpOTtVU7MVCi1qKg2cXFRc+Tkq+ufD/i0ikWtsZJ VZ8x8Y1ha079UjuV8WkGhPh8CfCsRkbVN5dVeY97Wlh15Y4/S6EV2Y7cDhwTOYj95RmfyQ16 3vV3IPQUGkHXKKudVqR8bKdrDWXMCcTLHMfaSJscefjy4mzyG3UpkKfJuuPAJJZnfWuRm6tm 2HiQDwWwuRM3ZRShs1X6Hie22r0zqUlWDLZ8ek+Y45IxgZwZYrgfpDxrFaCva8GI4GeQV2M+ nMDnqByDdzi77ndy0Rho81XRtlFAspp1hWC2DaD+LF/rlyQF4aLJ9w43d2HDB4B3jw4UTHoe lTPngha+YVeOnCnBYcuPd3tVZtzkfK+S4i+PhwxUjaoSsghHONg1HE+DXN8I0iw+KTRuftuZ 8rELpbE4YgyVvQ5lVJauNvxIZdynnxkrY8ibZ/8yBuj3NKjiI29GN843K+1Rrlhtsus+V2Lm /4Gbpfi40gBDYXWP3aPmaZNdwxiBSZgXvje9ZcHHtNv1yI8RwnN/deKke1/E2Gk9owJ/tr1E oaVAxEAkQWi3iCeeG1nqBlLMdvSYHq2llpjVQREALpi8yFLjV+HvfxDJagkN6Iq7vJixvNSR vwIMZfISPdWRziNv3xXYZDhpcYwPF6mlCCfDRqDOTIfRp9HQxCW29nGegC0yjICIBDqvuQDo pqh9Djhf7w9eypYAvzrNc2fl2GKgSBFmcZZfVf5Hd1ISUC9rKloM3PQi9E0EeEtKDLC5D2Q6 CiOCzxFp+OX+44R2/vKjJCisI2GPbZfHE1bPm+D9pewF3DQ0VSCyL96ctSjXG7iRkKt3469d 8B58uraDMQXuHpr769tDKdNz48lwtnk+o9h0QVvGUvUY2SRCr9PJmeM2e9NvPZvwoB1lBSXW EWd3MtzIpSMZd3YFWAOKDofbuis0e8enh/Q568XJGT4/CpGw6qVY35NPhWjiD1vE5UtCdkLm dwegc8x7xCzrjEIMdzc1yBdyDmqH0w6Cq4isskXPZ/vhg8V0Wp9WJ37CBGnxLGUat5JDFsmH S/MuorGmIZn5xTjd1gdKCHz+NRz1LU0hQBy7V4dJl62tMLPqd0p0TZwrzkmbARn4S9W8uB0O 2JUGVV/Dvye8xtFmPpBcjyJIFxHDkfI/Ebe9kY4zjzFbki3V17iKH82FvaN8Xs4rUNdXGl/1 5OJxFn1VQ3FeJnK4RIzfkp+udnPfMdU9DCeqPu4Hs+AIYY2UQDljoCqe2AMjRntWuE1u2Hqu sho+7xWRZDgFCtNvZA+NZaW5Y4QRD+AOmZGZ/Nrp4ENPGPEfQCNySq8EF+wduxNNs713xeBU eI2Hf12VjO6yCqqhRIYD/RVI7ZLwdgY1OBbcbbvfWM7o7+TqwRyi63p9w/8uj4PY85vmsMDO I/uZ2q8MmiPt0B1xU7Jjud5Y1SdX/dVRTfS/u6P9McxK6kiq8BpKEE77au1tS6aMSxh5BOlg znAbK73kc1nxZhdoI/3NqBlGQ+PCMjSUd6Q+1uZqOV+btLoMObPuTgKq1LhAR9kALsJV/lzl pWPqNTS3n6ZmJoTTEbihMCnO4RSwMe9Ts57E5jSF2ZLuzmGVOvHwQoxy0rhJbNnyNpit9SaH S2mY86ORPspctZ6xlgOTgNBEhwYWp/FXo25qQyT9/2zWwUgiyrZJ9aa9FjsX2FRVgkMH7bcU gbUmfKf1up0nbR2Ji0vJq9ZWsdjAVrZR6EZWcX7tmCYAkmWk1qygObeuiR62w7bKEuvMZjc0 cvJSCGrIV728OvNwcpCuoN/ggwPATwvyaMsd0Ya4Jhthyr8EGcCKv8HPI4bDo1P1Bb/z4z8e CqHeV5K5f8RhtiYWU6UDBXfsgaj6igmP974Inkw4xrRZX7mXcWPB7xu8iom6HBzEtcmICdLN vlGkkAc/DDoqn2qeQrXzvO+iOZjgPjdwxrkPGjjxtfqDU927aoijRRc8ckkacADO87InUTPY 2MyQAioha19pVHZSa5dRpKeJP3VUP4DAdnlgedjDeszY7mm8dA=
Ironport-hdrordr: A9a23:nwZQv6uWPm0sDBSDV0g1iZHY7skDT9V00zEX/kB9WHVpm62j5r mTdZEgvyMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniDhILAFugLhrcKgQeBJ8SUzJ876U 4PSdkZNDQyNzRHZATBjTVQ3+xO/DBPys6Vuds=
Ironport-phdr: A9a23:azz/9h9WJQlv9v9uWe22ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Y QqGv64m0wOBdL6YwswHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yeC/94fObwlWijexbrF/I RqrpgjNq8cahpdvJak2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3U bJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5 LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28d YsPCO8BMP5YoIn8o1sOqRq+ChOpBOjy1zFIh3r23ag90+QnCgHNwQstHtwVsHTVqdX1MaASU eauzKXSyDXMde9W2Tfm5YjHdxAuu/CMXbZqfcXNzkkvEhrIg1ONooPqIz2bzP4Cs3SH7+V+T +KvjXYqpx1vrjSxx8oihInHiIwbxF3A6Sl13Yg7KN26RUN4fdKpDJlduj+aOoZ2X84vQGNlt Tomx7AJpZO2YicHxYo6yxPZdveJfY+I4hf5W+aQJzd1nG5leby4hxap8EihxfH8Wdeo31ZKt CZKjt7MtnUL2hfO6caHUuNw8lm91TuLzQze6eFJLVopmafaN5It2KM8m5kOvUnFAyT4gl/5j LWMeUUh4uWo6/roYrHhppKEMo97kAD+MqA3lsymHeQ0LxECX2aG9em/ybHv50L5QLJNjv05l qnWrorWKtgcpq68GwNV04Aj5AijDzq+ztgUgX0KIEhGdR+HlYTlJlDDLOziAfuigFmgjS9nx /XcMb3gBpXNIGLDkLDkfbtl5U9c0wszzdVa55JTDLEBO+j/Wkrru9zEDh80KAO0w+P9B9V80 oMSQ36AAqicMK/Kt1+H/fogI/OQa48NpDb9N/8l6ubzgXMhg18SYbGp3YcLaHC/BvlpP0KZY WP1jtgdFWcKoxExQffxiFyCVD5Tf2y9U7g95jE9EoKmDJ3MSpqjgLybj2+HGchdYXkDAVSRG 1/pcZ+FUrECcnG8OMhkxwMFUbygQopp7hCrsQj80PIzMfHV/ygfs4ml0dFp58XckBgz8Xp/C MHLgDLFdH19gm5dH2x+56t4u0Eokj9rsIB9iv1cT5lI4u9RFx09PtjaxvB7DNb7XkTAeM2IQ RCoWIbuGik/G/Q2xdJGeENhA5O6lBmWwDGrBroSkafNAZUo8orT2nHwI4B2zHOVnLI5gQweS 9BUfXajmrY58gHSA4DTlEDMiL2rcKEb2jWL8W6fzUKBuUhZVEh7VqCWFWsHaB7wqtL0rljHU 6foCbkjNV5ZztWeL6JRdtDzpVBPRfOmIciHJmzoyz72ChGPybeBKoHtfg3xxQ37D04J20AW9 HeCb00lAzu55njZB3poHE7uZEXl9a9/rmm6Rwk61VPCaUopzLez9hMP4J7UA/oOwrIJvjsgo DRoDR682dzREd+Juwtmeu1Vf9o85F5N0W+RuRZ6O9SsKKVrh1hWdAoS3QumyA52D4BHl9Nsq Xo2zCJ9LKuZ1BVKcDbZlZH8N7vLK3XjqQi1Yv2zuBmW29KX96ETrfUg/g+77Uf5Swx7rS0hi okMgB7+rt3QAQEfUIz8SBMy/hl+/fTBZzUlopnT3jtqOLW1tTnL35QoAvEkw1CuZYQ6UuvMG QnsHskdH8XrJvYtng3jcQkFOeVV8rVyOsq6d9OJ3aeqOKBrmzfs3gElqMhtl1mB8SZxULuCw I0ExvSf2BDBUj7gjH+ut8n2ncZPYjRYTQ/dgWD0QYVWYKN1Z4MCD2yjdta2yttJjJnoQ3dE9 VSnCjvqweeRcAGJJxz41AxUjwEMpGC/3DG/xHpymi0oqayW2GrPxf7jfVwJIDwDSG5nhFbqa Y+66rJSFFezbg0skx2+o0Pz26hzq6F2Lm2VSkBNNyT7NGBtVKKsu6HKOZYersN193wJCKLlM QnSQ6WYwVNSyy75GmpC2D03PyqnvJn0hV0yiW6QKmpysGuMfMhxwRnF49mPIJwZljECRSR+l XzWHg3mZ4jvrYjSzsmb9LnuDjHENNUbayTgwIKeuTHu4GRrBUf6hPWvgpj9FgN81ybn1t5sX CGOrRDmY4Ct2b7pVIAvNkRuGlL47NJ3X49klY5lzo4L2H0fgZOOu38OjWfbPtBS2Ka4Z30ID 21uoZad8E3+1UtvI2jcjZ3iV3CYxc16IdyzfmM+1Sc07sQMA6CRpu8h/2M9sh+zqgTfZuJ4l zEWxK416XIUtOoOvRIk0iSXBr1BVVkdJyHnkA6EqsyvtKgCLnj6aqC+jQAt+LLpRKHHuAxXX 2z1P4svDTMlpNsqK0rCiTXy8t22I4SWNINL8EfIzFGYyLIJYJMpyqhU2Ww9Yjm75CN9jbZ81 E0Lv9nyvZDbeTszuvvhWFgAcGWyPZtb+ymx3/gA2JzKjsb/RtM5XW9TFJrwEaD3SnRL6bK+Z lzISHpl+hL5UfLeBVPNtxsg9iiSVcjtbzbOejEY1YkwHUHNYhUA30ZEGm19xMdxFxj2lpW+K wEgt2xXvhig7UISr4AgfxjnDjWF/FbuOmpyEcLPakIRt14K5l+JY5bHsKQuT2cBr8fn9EvUe ySaf1gaVzhXHBbfVha4ZP/2ooCRlorQTvy3K/+ECVmXgcpZUfrAhZem0488ui2JKt3KJH5pS fsyxktEW3l9XcXfgTQGDSINxWrLaIaAqRGw9zcSzIj3+en3WA/p+YqECqdDedRp9ReshK6fN umWzC9nIDdc35kIyDfG0r8alFIVjihvcXGqH9Fi/WbVS7nMn6ZMExMBQyZ6Nc8N9r5lmwcUa ZedhdTy2bp1yPUyDhYNVFDsnN2oed1fI2y5MwCiZg7DP7CHKDvXhsDvNPnkGPsA0aMN6UX24 GbCQCqBdnyZmjLkVg6iK7RJhSCfZllFvZ2lNwxqAi7lRc7nbRuyNJl2iyc3yPs6nCCvVyZUP D5ifkdKtrDV4zlfh6A1BHdA639iK/LCni+F78HXL58Xtb1gBSE+xIc4qDwqjqBY6i1JXqk/g CzJsttnuE2riMGKwztjFQNS83NF3dLS+0plPqrd+99LXnOOr3dvpS2ATh8NodViENjmvatdn 8POmKzEIzBH69vI/MEYCqA8yeqCOXsldAP1QXvaVVtcCzGsMm7bigpWl/TArhV9QbA1r5Htn NwFTboJDTTd89sVD01kGJoJJ5IlBlsZ
Ironport-sdr: 63d20901_9MUte0onicPbrCv1vuopBCT7I0vMKDHuXiaii91qfmTeP2Z FGp73htLdJvHzdkrqfQ6yyLkpGskWr1ssiTggcg==

(https://twosixtech.com/job/?gh_jid=4781892004)

Research Scientist - Formal Methods at Two Six Technologies

Arlington, Virginia

Two Six Technologies is seeking a Research Scientist - Formal Methods to research and develop high assurance software and hardware systems using advanced formal analysis technologies. We are seeking candidates with an interest in research as well as a commitment to developing solutions for the real world. Ideal candidates will have a passion for, and experience with, using concepts from pure mathematics in an industry setting.

Responsibilities

Prove safety and security properties of hardware and software
Learn and evaluate formal methods tools for use in verification tasks
Assist in writing research papers and conference talks on topics in formal methods
Work well independently in a small team and fast-paced environment
Collaborate with partners and customers to understand, tailor, and deliver solutions that meet their requirements

Qualifications

Advanced degree (Masters or PhD) in Computer Science, Computer/Electrical Engineering, Mathematics or related technical domain
Extensive experience working with any of the following, or similar, technologies:

Interactive theorem provers (e.g. Isabelle/HOL or Coq)
SMT solvers (e.g. Z3 or CVC4)

A foundational knowledge of software and systems engineeringA working knowledge of concepts from mathematical logic (higher-order logic, type theory)Comfortable working as part of a small development team composed of researchers, engineers, and scientistsFamiliarity with functional languagesStrong oral and written communication skillsAbility to obtain and maintain DoD security clearance

Nice to haves

Modern cryptography domain experience and knowledge
Experience developing cybersecurity solutions and products

On Wed, Jan 25, 2023 at 9:37 PM Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

Suppose an undergraduate or MS student gets entranced by Cow, Lean, formalizing math, etc. But they do also ask, "For what jobs at what places might I reasonably expect to be prepared by virtue of having learned logic, languages, reasoning, and maths stuff?" An appeal to anyone who might add an entry here, in response. Thank you in advance. --Kevin Sullivan, UVA CS

[Coq-Club] Jobs for undergrads / MS students with proof chops, Kevin Sullivan, 01/26/2023
- Re: [Coq-Club] Jobs for undergrads / MS students with proof chops, William Simmons, 01/26/2023
- Re: [Coq-Club] Jobs for undergrads / MS students with proof chops, mukesh tiwari, 01/26/2023
  - Re: [Coq-Club] Jobs for undergrads / MS students with proof chops, Alyssa N Byrnes, 01/26/2023
    - Re: [Coq-Club] Jobs for undergrads / MS students with proof chops, Alexander Gryzlov, 01/26/2023